From 367ae7c6fc0a622e96902aa035cea22e3ecb119c Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 30 Apr 2024 17:13:14 +0100 Subject: [PATCH] Remove theorem prover targets from default Makefile rule 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. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 7068968f4..3f5e92665 100644 --- a/Makefile +++ b/Makefile @@ -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