From 08f96f61a6578c9fe45acb4fb9b42af680e77d21 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 10 May 2024 03:16:06 +0100 Subject: [PATCH] Remove theorem prover targets from default Makefile rule (#464) 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 a7e441e67..32073dd84 100644 --- a/Makefile +++ b/Makefile @@ -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