Skip to content

Commit

Permalink
Remove theorem prover targets from default Makefile rule (#464)
Browse files Browse the repository at this point in the history
In general we aren't requiring contributors to implement the correct
Lem/Isabelle/HOL4/Coq stubs for new extensions (this would almost
certainly be way too high a bar) so having these in the default set of
build targets just means that typing 'make' is broken until those of us
who are invested in maintaining those targets can add updates for those
stubs.
  • Loading branch information
Alasdair committed May 10, 2024
1 parent e3c5b0a commit 08f96f6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -201,7 +201,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))

.PHONY:

all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) riscv_isa riscv_coq riscv_hol riscv_rmem
all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH)
.PHONY: all

# the following ensures empty sail-generated .c files don't hang around and
Expand Down

0 comments on commit 08f96f6

Please sign in to comment.