Dune build
Things to do before this can be merged:
Blocker:
-
Make CI work -
Make timing runner in CI work -
Check that CI that tests against iris master still works -
Figure out the right command to build examples in RefinedC repo -
make && make install && refinedc check example.c
: Probably suboptimal? -
dune exec -- refinedc check --no-build example.c && dune build
: Rebuilds everything -
dune exec -- refinedc check --no-build example.c && dune build $(dirname example.c)
: Does this work? No - Can one add an option to print
output_dir
?
-
-
Figure out if one can get rid of the dune
files in the directories. Probably not... -
Can manual proof files live in a different folder than the generated files? - Seems very hard because dune does not allow cycles between modules -
Is there a way to write a .gitignore file that ignores all generated files? Ignore code.v
,spec.v
andproof_*.v
-
Rename +rc+
to something else-
proof
?rc
?
-
-
Make all generated files start with rc_
?
Nice to have but not important for first version:
-
Make path where generated files land configurable - Minimal version: Allow user to pick a different directory name than
+rc+
- Advanced version: Allow the user to give a path where the generates files should live
- if the path starts with
/
, it is relative to the root of the repo, otherwise it is relative to the dir of the file - the path can contain
{FILENAME}
which gets replaced by the filename of the generated file - examples:
-
+rc+/{FILENAME}/
current version -
/generated/{FILENAME}_
(note no trailing slash) all generated files land in thegenerated
folder
-
- if the path starts with
- Minimal version: Allow user to pick a different directory name than
-
Display the running time after compiling a file (similar to TIMED=y make
)
Also nice to have, but not so important:
-
Display a message when dune starts running a command (compared to only when the command is done)
Edited by Michael Sammler