Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

wip: Use Dune as primary build system #29

wants to merge 1 commit into
base: master


None yet
1 participant
Copy link

commented May 7, 2019

This cannot be completed until Dune support “compositional build” for Coq projects.

@lthms lthms force-pushed the lthms:dune branch from 7660e37 to 23e532b May 9, 2019

@lthms lthms marked this pull request as ready for review May 9, 2019

@lthms lthms force-pushed the lthms:dune branch 5 times, most recently from c34244d to 86f18f9 May 9, 2019

@lthms lthms force-pushed the lthms:dune branch from 86f18f9 to 320ae93 May 9, 2019


This comment has been minimized.

Copy link
Contributor Author

commented May 9, 2019

The current setup provides the same build features as the Makefile-based approach that we are currently using, but it is clearly intended according to the Coq developers that dune becomes the preferred tool to build Coq project.

Current +:

  • Everything in _build, nothing in src and theories directories
  • As soon as “compositional build” for Coq are supported, dependencies between FreeSpec components will be way more easier to deal with (eg. if FreeSpec.Core gets some change, dune will now that it has to build FreeSpec.Exec)

Current -:

  • ProofGeneral expects .vo and .glob files to be available in theories/, so it basically compiles again. That is annoying, and I wonder if there are plans to support _build/ directory by PG
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.