Rocq 9.0.0

[shilangyu]

TODO:

• alectryon does not work, SerAPI does not support Rocq 9.0.0: Alectryon for Rocq 9.0 cpitclaudel/alectryon#104
• There are some warnings regarding Focus.v Notation having conflicts
• Double check extraction works correctly
• Double check if the nix flake needs updates

When the new dune plugin is released, we can use ocaml/dune#11752

[Ef55]

Glad to see Warblre updated to Rocq!

FYI the pull request you pointed to was merged a few hours ago (may still take some time before a new version of dune gets released though).

I attempted to update the flake to Rocq 9.1, but it would seem I've somehow run into rocq-prover/rocq#20128 :

Details

dune build
File "engines/ocaml/dune", lines 10-13, characters 0-102:
10 | (coq.extraction
11 |  (prelude Extraction)
12 |  (extracted_modules Extracted)
13 |  (theories Warblre Ltac2 Stdlib))
*** Error: Anomaly
           "Uncaught exception Fl_package_base.No_such_package("rocq-runtime", "")."
           Please report at http://rocq-prover.org/bugs/.
File "mechanization/dune", lines 3-6, characters 0-72:
3 | (coq.theory
4 |  (name Warblre)
5 |  (package warblre)
6 |  (theories Ltac2 Stdlib))
*** Error: Anomaly
           "Uncaught exception Fl_package_base.No_such_package("rocq-runtime", "")."
           Please report at http://rocq-prover.org/bugs/.
File "engines/js/dune", lines 10-13, characters 0-102:
10 | (coq.extraction
11 |  (prelude Extraction)
12 |  (extracted_modules Extracted)
13 |  (theories Warblre Ltac2 Stdlib))
*** Error: Anomaly
           "Uncaught exception Fl_package_base.No_such_package("rocq-runtime", "")."
           Please report at http://rocq-prover.org/bugs/.

It seems to just be the latest nix issue related to the Rocq renaming. I don't think there is anything we can do on our side, so I'd be tempted to tell you to disregard this issue, as long as everything else is working.

[shilangyu]

Thanks for the flake update Noé :)

It seems to just be the latest nix issue related to the Rocq renaming. I don't think there is anything we can do on our side, so I'd be tempted to tell you to disregard this issue, as long as everything else is working.

We have to wait for alectryon, maybe by that time nix will get fixed

FYI the ocaml/dune#12035 you pointed to was merged a few hours ago (may still take some time before a new version of dune gets released though).

I think yes, it might take a while. I will keep a close eye.

[shilangyu]

The new dune might be released soon: ocaml/dune#12788 (comment)

I pushed a WIP commit (won't compile unless you upgrade dune with opam pin add dune.3.21.0 https://github.com/ocaml/dune.git#6e9d965bb5bbadfe9cbf89314cb6f8ecaa845bd9). It migrates to the new dune plugin. I also removed all _CoqProject files. I am not sure they are useful at all since we are using dune anyway? If it is useful, we can consider instead using the dune's (generate_project_file) option which would generate it automatically.

[Aurele-Barriere]

Thanks a lot! The _CoqProject file is actually useful for some editors, I think proof-general uses it for instance.
I didn't know about dune's generate_project_file, that could be a better way yes!

[shilangyu]

Thanks a lot! The _CoqProject file is actually useful for some editors, I think proof-general uses it for instance. I didn't know about dune's generate_project_file, that could be a better way yes!

I can enable it, but just for clarity: I don't think it produces commitable files. They contain absolute paths (I wonder if it is even expected). So users will have to run dune build first (which, I think is a fair requirement)

[Aurele-Barriere]

Running dune build first seems fair to me too

[Ef55]

Some updates:

• I updated the nix stuff to use the "bleeding-edge" versions of rocq/dune. Seems like everything builds successfully on my end now! I'll have to tweak the nix files again once these bleeding-edge versions become available in nixpkgs (we don't need to wait for that to merge though).

• I fixed many (if not all) of the new warnings.

• I double checked that _RocqProject was needed; generate_project_file works great though.

• I'm getting this big message in my terminal when running dune build, which I don't remember happening in the past (I may be misremembering though):

  Details

       = Success                            
           (NonGlobalResult
              (Exotic
                 (exec_array_exotic 2 [104; 101; 108; 108; 111] [
                    Some [108]] None None None)))
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.039 secs (0.037u,0.001s) (successful)
       = Success (NonGlobalResult Null)
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.003 secs (0.003u,0.s) (successful)
       = Success
           (NonGlobalResult
              (Exotic
                 (exec_array_exotic 2 [104; 101; 108; 108; 111]
                    [Some [108; 108]] None None None)))
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.03 secs (0.03u,0.s) (successful)
       = Success
           (NonGlobalResult
              (Exotic
                 (exec_array_exotic 0 [97; 98] [Some [97; 98]] None None None)))
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.051 secs (0.051u,0.s) (successful)
       = Success
           (NonGlobalResult
              (Exotic
                 (exec_array_exotic 0 [97; 98] [Some [97; 98]; Some [98]]
                    (Some []) None None)))
       : Result ProtoMatchResult Errors.MatchError.type
  Finished transaction in 0.074 secs (0.071u,0.002s) (successful)
  

• I (finally) reported the melange warning: Using new.target in raw JS results in a warning melange-re/melange#1685

• For some reason I have yet to understand, our extraction hacks to map Rocq's bigints to Ocaml/Js bigints stopped working properly (run dune test to see failing tests). I'll take another look later this week.

• Change SpecMerger remote&commit in flake once Bump versions in nix flake SpecMerger#2 is merged

[shilangyu]

Thank you!

1. Regarding the message, it seems to have been present before this PR already (see the dune build step): https://github.com/epfl-systemf/Warblre/actions/runs/18123838898/job/51574355291?pr=5
2. We merged your SpecMerger PR

[Ef55]

1. Great, one less thing to fix!
2. I'll update the flake, thx

[Ef55]

OK, I figured out where the extraction issue came from: it was caused by the split of the Pos library into two pieces (one in the Corelib, the other in the Stdlib), which caused some weirdness in the extraction.

Everything seems good on my side. I guess the last thing to fix is the CI (and re-enabling alectryon when it gets updated). @shilangyu will you take care of the CI, or should I take a look? The current failure seems related to the install of dune, which means you might be better geared to investigate than I am (since the CI does not use nix).

[shilangyu]

Thanks for the extraction fix! I think now we just wait for alectryon. The CI is failing because we now use the unreleased dune version (which just got an alpha release). Once it is released, the CI will work again.