fix: failing coq --config #8966
Conversation
|
Thanks a lot Ali! I will review tomorrow (if you need a review) |
|
@ejgallego A look over would be nice. I think just reading what I've written in the test and whether that makes sense would be enough. |
|
Thanks @Alizter ! |
There was a problem hiding this comment.
LGTM, thanks Ali! I let you merge.
I wonder if maybe a general mechanism to query this kind of programs, and handle errors in the same way would be of interest to Dune?
We could have helpers to implement some common operations, for example, to provide default values.
|
@ejgallego If you have a look, its easy to see that coq_config is inspired by the handling in OCaml. I don't see much utility in sharing code here as each has very specific needs. |
|
Before we merge, I need to push a changelog entry. |
Indeed, sorry I forgot about this! Regarding the handling of the commands, I was thinking more about making an extension of But indeed not a lot to gain right now I think? It seems dune has about 50 uses of it, so I'm unsure. |
487ede8 to
1f89ef1
Compare
|
I've added a changelog entry. @rgrinberg can you take a quick look and/or merge? |
|
@Alizter what's blocking this? I'd suggest amending a bit the changes entry, otherwise I suggest we merge. |
|
@ejgallego I can't amend the changelog just yet. So if you want to do it feel free. There is nothing else blocking this AFAIK. |
|
@Alizter sounds good, I will amend and merge if I get a minute, otherwise you feel free to go ahead. |
Signed-off-by: Ali Caglayan <alizter@gmail.com>
1f89ef1 to
bfa803b
Compare
We fix a bug where coqc --config or --print-version would fail in some situations leaving the user with a half baked message and no clear way forward. This can happen for example when using only coq-core. In order to fix this, we make config return a more principled result type allowing consumers of the API to handle such errors in a better fashion. We also now pass `-boot` to `coqc --print-version` which is identical, but works around a bug in Coq which caused failures when only coq-core is installed. We also improve various error messages that occur when Dune's internal queries to coqc fail. Signed-off-by: Ali Caglayan <alizter@gmail.com>
bfa803b to
1247850
Compare
CHANGES: - Introduce `$ dune ocaml doc` to open and browse documentation. (ocaml/dune#7262, fixes ocaml/dune#6831, @EmileTrotignon) - `dune cache trim` now accepts binary byte units: `KiB`, `MiB`, etc. (ocaml/dune#8618, @Alizter) - No longer force colors for OCaml 4.03 and 4.04 (ocaml/dune#8778, @rgrinberg) - Introduce new experimental odoc rules (ocaml/dune#8803, @jonjudlam) - Introduce the `runtest_alias` field to the `cram` stanza. This allows removing default `runtest` alias from tests. (@rgrinberg, ocaml/dune#8887) - Do not ignore libraries named `bigarray` when they are defined in conjunction with OCaml 5.0 (ocaml/dune#8902, fixes ocaml/dune#8901, @rgrinberg) - Dependencies in the copying sandbox are now writeable (ocaml/dune#8920, @rgrinberg) - Absent packages shouldn't prevent all rules from being loaded (ocaml/dune#8948, fixes ocaml/dune#8630, @rgrinberg) - Correctly determine the stanza of menhir modules when `(include_subdirs qualified)` is enabled (@rgrinberg, ocaml/dune#8949, fixes ocaml/dune#7610) - Display cache location in Dune log (ocaml/dune#8974, @nojb) - Re-run actions whenever `(expand_aliases_in_sandbox)` changes (ocaml/dune#8990, @rgrinberg) - Rules that only use internal dune actions (`write-file`, `echo`, etc.) can now be sandboxed. (ocaml/dune#9041, fixes ocaml/dune#8854, @rgrinberg) - Do not re-run rules when their location changes (ocaml/dune#9052, @rgrinberg) - Correctly ignore `bigarray` on recent version of OCaml (ocaml/dune#9076, @rgrinberg) - Add `test_` prefix to default test name in `dune init project` (ocaml/dune#9257, fixes ocaml/dune#9131, @9sako6) - Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting of workspace-wide defaults for `coqdoc_flags`. (ocaml/dune#9280, fixes ocaml/dune#9139, @Alizter) - [coq rules] Be more tolerant when coqc --print-version / --config don't work properly, and fallback to a reasonable default. This fixes problems when building Coq projects with `(stdlib no)` and likely other cases. (ocaml/dune#8966, fix ocaml/dune#8958, @Alizter, reported by Lasse Blaauwbroek) - Dune will now run at a lower framerate of 15 fps rather than 60 when `INSIDE_EMACS`. (ocaml/dune#8812, @Alizter) - dune-build-info: when `version=""` is found in a `META` file, we now return `None` as a version string (ocaml/dune#9177, @emillon) - Dune can now be built and installed on Haiku (ocaml/dune#8795, fix ocaml/dune#8551, @Alizter) - Mark installed directories in `dune-package` files. This fixes `(package)` dependencies against packages that contain such directories. (ocaml/dune#8953, fixes ocaml/dune#8915, @emillon)
The first commit adds a test detailing how Dune reacts to
coqc --versionandcoqc --configfailing. We write down what we expect to happen in each situation.The second commit does a few things:
coq_configis handled, shares more code, streamlines the API (removingmake_exn).-boottocoqc --print-versionto make it work when onlycoq-coreis around.coqc --configdoes not inhibit the build. There is a check for the config in the installed theories composition for example. We emit a warning if config fails and do a best effort without any installed theories.I don't think this needs a version bump as it affects a very small minority of users who build with only
coq-core.(stdlib no)broken since 3.8.0 #8958