diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 14 |
1 files changed, 10 insertions, 4 deletions
@@ -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)) |