Skip to content

Commit

Permalink
Remove theorem prover targets from default Makefile rule
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 Apr 30, 2024
1 parent c5ee87d commit 367ae7c
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 @@ -199,7 +199,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 367ae7c

Please sign in to comment.