Merge branch 'main' into option-take

1 files changed, 10 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index 0f3e2999..08359d49 100644
--- a/Makefile
+++ b/Makefile
@@ -31,9 +31,8 @@ AENEAS_EXE ?= bin/aeneas
 
 # The user can specify additional translation options for Aeneas.
 # By default we activate the (expensive) sanity checks.
-OPTIONS ?= -checks
+OPTIONS ?=
 
-#
 # The rules use (and update) the following variables
 #
 # The Charon test directory where to look for the .llbc files
@@ -84,7 +83,7 @@ doc:
 	cd compiler && dune build @doc
 
 .PHONY: clean
-clean:
+clean: clean-generated
 	cd compiler && dune clean
 
 # Test the project by translating test files to F*
@@ -100,6 +99,12 @@ test-all: test-no_nested_borrows test-paper \
 	test-loops \
 	test-arrays test-traits test-bitwise test-demo
 
+.PHONY: clean-generated
+clean-generated:
+	# We can't put this line in `tests/Makefile` otherwise it will detect itself.
+	# FIXME: generation of hol4 files is deactivated so we don't delete those.
+	grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm
+
 # Verify the F* files generated by the translation
 .PHONY: verify
 verify:
@@ -108,7 +113,8 @@ verify:
 # Reformat the project
 .PHONY: format
 format:
-	cd compiler && dune build @fmt --auto-promote
+	@# `|| `true` because the command returns an error if it changed anything, which we don't care about.
+	cd compiler && dune fmt || true
 
 # The commands to run Charon to generate the .llbc files
 ifeq (, $(REGEN_LLBC))