Skip to content

fix(coq): fix crash when COQ_NATIVE_COMPILER_DEFAULT missing #7847

Merged
Alizter merged 5 commits intoocaml:mainfrom
Alizter:ps/branch/fix_coq___better_config_var_not_found_message
Jun 1, 2023
Merged

fix(coq): fix crash when COQ_NATIVE_COMPILER_DEFAULT missing #7847
Alizter merged 5 commits intoocaml:mainfrom
Alizter:ps/branch/fix_coq___better_config_var_not_found_message

Conversation

@Alizter
Copy link
Copy Markdown
Collaborator

@Alizter Alizter commented May 31, 2023 •
edited
Loading

Coq versions < 8.13 do not have COQ_NATIVE_COMPILER_DEFAULT and were causing dune to crash when searching for this var. We make it so that if dune does not find it, it defaults to "no". The docs should also be updated accordingly.

fix #7846

  • changelog
  • docs (need to mention native comp not supported < 8.13)

@Alizter Alizter changed the title fix(coq): better config var not found message fix(coq): fix crash when COQ_NATIVE_COMPILER_DEFAULT missing May 31, 2023
@Alizter Alizter requested a review from ejgallego May 31, 2023 17:44
@Alizter Alizter added the coq label May 31, 2023
@Alizter Alizter force-pushed the ps/branch/fix_coq___better_config_var_not_found_message branch from 50deed8 to 50a0492 Compare May 31, 2023 17:54
@Alizter Alizter requested a review from christinerose as a code owner May 31, 2023 17:54
@Alizter Alizter force-pushed the ps/branch/fix_coq___better_config_var_not_found_message branch from 50a0492 to eac2e77 Compare May 31, 2023 17:55
This was referenced May 31, 2023
Closed
Closed
@erikmd
Copy link
Copy Markdown

erikmd commented May 31, 2023 •
edited
Loading

Thanks @Alizter, but I'm not sure the fix is optimal.

Namely, coqc supports -native-compiler yes for 8.5 ≤ Coq ≤ 8.12 as well.

The only change is that starting from Coq ≥ 8.13, is that the coqc flag is optional provided it has been provided to ./configure (e.g. via the coq-native package flag).

For more context, see:

@erikmd
Copy link
Copy Markdown

erikmd commented May 31, 2023

To sum up, the expected behavior (already applied by coq-makefile) would be something like this:

  • if Coq ≥ 8.13 has been compiled with a -native-compiler … flag, dune would automatically generate .coq-native/* files
  • if 8.5 ≤ Coq ≤ 8.13, it would do so as well, but only if (mode native) is manually provided.

Cc @proux01 @ejgallego FYI

@Alizter
Copy link
Copy Markdown
Collaborator Author

Alizter commented May 31, 2023 •
edited
Loading

This won't mean that (mode native) will stop working for older versions of Coq however. What this changes is the detection of native from how coq was configured which I only know to be exposed via the configure variable as you said. This detection only happens if a (mode ) field was not provided.

proux01
proux01 approved these changes Jun 1, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@proux01 proux01 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, thanks

@LasseBlaauwbroek
Copy link
Copy Markdown
Contributor

LasseBlaauwbroek commented Jun 1, 2023

This patch works for me. Thanks @Alizter.

ejgallego
ejgallego approved these changes Jun 1, 2023
View reviewed changes
Copy link
Copy Markdown
Collaborator

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @Alizter !

I think we may have a problem in the API tho, it seems to me that for variables that may not be present, we should have the config record reflect this using option, and the rules can actually try to figure out what the right action to perform is based on the coq lang version and on the rules at play. I find this a bit more robust.

So if you want to tweak that, that's fine, not a big deal otherwise.

@ejgallego ejgallego assigned ejgallego and Alizter and unassigned ejgallego Jun 1, 2023
@Alizter
Copy link
Copy Markdown
Collaborator Author

Alizter commented Jun 1, 2023

@ejgallego good point, I'll move the selection to the rules to separate concerns.

@Alizter Alizter force-pushed the ps/branch/fix_coq___better_config_var_not_found_message branch from eac2e77 to 81a91c3 Compare June 1, 2023 16:19
Alizter added 4 commits June 1, 2023 18:20
@Alizter
fix(coq): better config var not found message
becd269 
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter
fix(coq): fix crash when COQ_NATIVE_COMPILER_DEFAULT missing
a8a0d21 
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter
doc(coq): update documentation about native compilation wrt old coq ver
7b22098 
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter
coq: encapsulate value type in coq_config
35a75bd 
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter Alizter force-pushed the ps/branch/fix_coq___better_config_var_not_found_message branch from 81a91c3 to 35a75bd Compare June 1, 2023 16:20
@Alizter
Copy link
Copy Markdown
Collaborator Author

Alizter commented Jun 1, 2023

I've tweaked the API a bit so that the decision on what to do with missing values lies on the user.

@Alizter Alizter merged commit d37f293 into ocaml:main Jun 1, 2023
@Alizter Alizter deleted the ps/branch/fix_coq___better_config_var_not_found_message branch June 1, 2023 18:49
@Alizter Alizter added this to the 3.8.1 milestone Jun 1, 2023
@Alizter Alizter mentioned this pull request Jun 2, 2023
Closed
4 tasks
emillon added a commit that referenced this pull request Jun 5, 2023
@emillon @Alizter
[3.8] backport #7847 (#7888)
f77e3b5 
* fix(coq): better config var not found message

Signed-off-by: Ali Caglayan <alizter@gmail.com>

* fix(coq): fix crash when COQ_NATIVE_COMPILER_DEFAULT missing

Signed-off-by: Ali Caglayan <alizter@gmail.com>

* doc(coq): update documentation about native compilation wrt old coq ver

Signed-off-by: Ali Caglayan <alizter@gmail.com>

* coq: encapsulate value type in coq_config

Signed-off-by: Ali Caglayan <alizter@gmail.com>

---------

Signed-off-by: Ali Caglayan <alizter@gmail.com>
Co-authored-by: Ali Caglayan <alizter@gmail.com>
emillon added a commit to emillon/opam-repository that referenced this pull request Jun 5, 2023
@emillon
[new release] dune (15 packages) (3.8.1)
ea834d8 
CHANGES:

- Fix a crash when using a version of Coq < 8.13 due to the native compiler
  config variable being missing. We now explicitly default to `(mode vo)` for
  these older versions of Coq. (ocaml/dune#7847, fixes ocaml/dune#7846, @Alizter)

- Duplicate installed Coq theories are now allowed with the first appearing in
  COQPATH being preferred. This is inline with Coq's loadpath semantics. This
  fixes an issue with install layouts based on COQPATH such as those found in
  nixpkgs. (ocaml/dune#7790, @Alizter)

- Revert ocaml/dune#7415 and ocaml/dune#7450 (Resolve `ppx_runtime_libraries` in the target context when
  cross compiling) (ocaml/dune#7887, fixes ocaml/dune#7875, @emillon)
@emillon emillon mentioned this pull request Jun 5, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ejgallego ejgallego ejgallego approved these changes

+2 more reviewers

@christinerose christinerose christinerose approved these changes

@proux01 proux01 proux01 approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@Alizter Alizter

Labels

coq

Projects

None yet

Milestone

3.8.1

Development

Successfully merging this pull request may close these issues.

[Coq] Dune crashes on version 3.8

6 participants

@Alizter @erikmd @LasseBlaauwbroek @ejgallego @christinerose @proux01