Skip to content

Dune build

Michael Sammler requested to merge dune_build into master

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 and proof_*.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 the generated folder
  • 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

Merge request reports