Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • RefinedC RefinedC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 21
    • Issues 21
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 3
    • Merge requests 3
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Metrics
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • RefinedCRefinedC
  • Merge requests
  • !2

Dune build

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Michael Sammler requested to merge dune_build into master Sep 22, 2020
  • Overview 1
  • Commits 29
  • Pipelines 16
  • Changes 356

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 Oct 01, 2020 by Michael Sammler
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: dune_build