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.

Sign up for GitHub

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

feature(coq): composition of installed theories #7047

Merged
merged 7 commits into from
Apr 20, 2023
Merged

feature(coq): composition of installed theories #7047

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
de67c0d
improve scrubbing script
Alizter Mar 18, 2023
216f957
refactor(coq_lib): refine api for dune coq libraries
Alizter Mar 6, 2023
84704c4
coq_lib: Use Path.t rather than Path.Build.t for Id.t.
Alizter Mar 7, 2023
ab2cd61
coq_lib: improve error messages
Alizter Mar 7, 2023
d6dd9f9
refactor(coq_lib): Refine library resolution result types
Alizter Mar 7, 2023
83f5cbe
coq_lib_name: add and expose some functions for installed composition
Alizter Mar 6, 2023
49c35b0
feature(coq): composition of installed theories
Alizter Mar 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,10 @@ Unreleased
- Dune in watch mode no longer builds concurrent rules in serial (#7395
@rgrinberg, @jchavarri)

- Dune can now detect Coq theories from outside the workspace. This allows for
composition with installed theories (not necessarily installed with Dune).
(#7047, @Alizter, @ejgallego)

- `dune coq top` now correctly respects the project root when called from a
subdirectory. However, absolute filenames passed to `dune coq top` are no
longer supported (due to being buggy) (#7357, fixes #7344, @rlepigre and
Expand Down
Loading