Janno/test 21247

.github/workflows/sl-fm-ci.yml

@@ -0,0 +1,11 @@
+name: CI
+on:
+  push:
+    branches: ["main", "skylabs-*"]
+  pull_request:
+    types: [synchronize,opened,reopened]
+
+jobs:
+  CI:
+    uses: SkylabsAI/workspace/.github/workflows/filter.yml@main
+    secrets: inherit

.gitignore

@@ -158,6 +158,4 @@ bin
 *.install
 
 .dune-stamp
-/theories/Corelib/dune
-/theories/Ltac2/dune
 /test-suite/test_suite_config.inc

.gitlab-ci.yml

@@ -40,8 +40,8 @@ variables:
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
-  BASE_CACHEKEY: "old_ubuntu_lts-V2025-04-29-b90c41d539"
-  EDGE_CACHEKEY: "edge_ubuntu-V2025-04-07-dee2054641"
+  BASE_CACHEKEY: "old_ubuntu_lts-v9.1-V2025-04-29-b90c41d539"
+  EDGE_CACHEKEY: "edge_ubuntu-v9.1-V2025-04-07-dee2054641"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 

.mailmap

@@ -9,10 +9,12 @@
 ## If you're mentioned here and want to update your information,
 ## either amend this file and commit it, or contact the coqdev list
 
+Wassim Ait-Moussa <dragonballwassim01@gmail.com>   blumer <dragonballwassim01@gmail.com>
 Guillaume Allais <guillaume.allais@ens-lyon.org>   gallais <guillaume.allais@ens-lyon.org>
 Abhishek Anand <abhishek.anand.iitg@gmail.com>     Abhishek Anand (@brixpro-home) <abhishek.anand.iitg@gmail.com>
 Abhishek Anand <abhishek.anand.iitg@gmail.com>     Abhishek Anand (optiplex7010@home) <abhishek.anand.iitg@gmail.com>
 Léo Andrès <leo@ndrs.fr>                           zapashcanon <leo@ndrs.fr>
+Florian Angeletti < >                              Octachron
 Jim Apple <github.public@jbapple.com>              jbapple <github.public@jbapple.com>
 Bruno Barras <bruno.barras@inria.fr>               barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Bruno Barras <bruno.barras@inria.fr>               barras-local <barras-local@85f007b7-540e-0410-9357-904b9bb8a0f7>
@@ -56,6 +58,8 @@ Juan Conejero <juanconrod@protonmail.com>                 Juan C <juanconrod@pro
 Pierre Corbineau <Pierre.Corbineau@NOSPAM@imag.fr> corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Judicaël Courant <courant@gforge>                  courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Pierre Courtieu <Pierre.Courtieu@cnam.fr>          courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Pierre Courtieu <Pierre.Courtieu@cnam.fr>          Matafou
+Julien Cretin <github@ia0.eu>                      ia0 <git@ia0.eu>
 David Delahaye <delahaye@gforge>                   delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Maxime Dénès <mail@maximedenes.fr>                 mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Maxime Dénès <mail@maximedenes.fr>                 Maxime Denes <maximedenes@gillespie.inria.fr>
@@ -71,6 +75,7 @@ Louise Dubois de Prisque < >                       louiseddp
 formalize.eth <formalize@protonmail.com>           ilya <ilya@localhost.localdomain>
 Andres Erbsen <andreser@mit.edu>                   Andres Erbsen <andres@kevix.co>
 Andres Erbsen <andreser@mit.edu>                   andres-erbsen <andres-erbsen@users.noreply.github.com>
+Jian Fang <hufangyu123@gmail.com>                  Rw1nd <hufangyu123@gmail.com>
 Jim Fehrle <jim.fehrle@gmail.com>                  Jim <jfehrle@sbcglobal.net>
 Jim Fehrle <jim.fehrle@gmail.com>                  Jim Fehrle <jim.fehrle@gmail.com>
 Jim Fehrle <jim.fehrle@gmail.com>                  jfehrle <jfehrle@users.noreply.github.com>
@@ -133,6 +138,7 @@ Evgenii Kosogorov <284661@niuitmo.ru>              doctor-kaliy
 Ethan A. Kuefner <ek@conjectu.red>                 e kuefner <ek@conjectu.red>
 Ambroise Lafont <chaster_killer@hotmail.fr>        amblaf <you@example.com>
 Ambroise Lafont <chaster_killer@hotmail.fr>        Ambroise <chaster_killer@hotmail.fr>
+Lucie Lahaye <github@tweqx.fr>                     Lucie <github@tweqx.fr>
 Thomas Lamiaux < >                                 thomas-lamiaux
 Vincent Laporte <Vincent.Laporte@inria.fr>         Vincent Laporte <Vincent.Laporte@gmail.com>
 Vincent Laporte <Vincent.Laporte@inria.fr>         Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
@@ -143,6 +149,7 @@ William Lawvere <mundungus.corleone@gmail.com>     william-lawvere <mundungus.co
 Larry Darryl Lee Jr. <llee454@gmail.com>           llee454@gmail.com <llee454@gmail.com>
 Larry Darryl Lee Jr. <llee454@gmail.com>           Larry D. Lee Jr <llee454@gmail.com>
 Rodolphe Lepigre <rodolphe@bedrocksystems.com>     rlepigre
+Rodolphe Lepigre <rodolphe@bedrocksystems.com>     rlepigre-skylabs-ai
 Xavier Leroy <xavier.leroy@college-de-france.fr>   Xavier Leroy <xavier.leroy@inria.fr>
 Pierre Letouzey <pierre.letouzey@inria.fr>         letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Pierre Letouzey <pierre.letouzey@inria.fr>         letouzey <pierre.letouzey@inria.fr>
@@ -167,6 +174,7 @@ Erik Martin-Dorel <erik.martin-dorel@irit.fr>      Erik Martin-Dorel <erik@marti
 Erik Martin-Dorel <erik.martin-dorel@irit.fr>      erikmd <erikmd@users.noreply.github.com>
 Julien Narboux <jnarboux@gforge>                   jnarboux <jnarboux@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Julien Narboux <jnarboux@gforge>                   narboux <narboux@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Patrick Nicodemus < >                              patrick-nicodemus
 Jean-Marc Notin <notin@gforge>                     notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty <notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Charles Norton <arthur@chargueraud.org>            CharlesCNorton <135471798+CharlesCNorton@users.noreply.github.com>
 Jean-Marc Notin <notin@gforge>                     notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>
@@ -203,11 +211,13 @@ Jean-Pierre Rodi <jprodi04@gmail.com>              Fourchaux <jprodi04@gmail.com
 Pierre Rousselin <rousselin@math.univ-paris13.fr>  Villetaneuse <Villetaneuse@users.noreply.github.com>
 Pierre Roux <pierre@roux01.fr>                     Pierre Roux <pierre.roux@onera.fr>
 Pierre Roux <pierre@roux01.fr>                     proux01 <proux01@users.noreply.github.com>
+Radosław Rowicki <radrowicki+github@gmail.com>     radrow <radrowicki@gmail.com>
 Matthew Ryan <mr_1993@hotmail.co.uk>               mrmr1993 <mr_1993@hotmail.co.uk>
 Claudio Sacerdoti Coen <sacerdot@gforge>           sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Kazuhiko Sakaguchi <pi8027@gmail.com>              Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp>
 Kazuhiko Sakaguchi <pi8027@gmail.com>              Kazuhiko Sakaguchi <sakaguchi@peano-system.jp>
 Kazuhiko Sakaguchi <pi8027@gmail.com>              pi8027 <pi8027@users.noreply.github.com>
+Gabriel Scherer < >                                gasche
 Marcello Seri <mseri@users.noreply.github.com>
 Vincent Siles <vsiles@gforge>                      vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Kartik Singhal <kartiksinghal@gmail.com>           Kartik Singhal <ks@cs.uchicago.edu>
@@ -226,6 +236,7 @@ Paul Steckler <steck@stecksoft.com>                Paul Steckler <psteck@mit.edu
 Frank Steffahn <fdsteffahn@gmail.com>              staffehn <fdsteffahn@gmail.com>
 Sergei Stepanenko <kaptch@gmail.com>               Kaptch <kaptch@gmail.com>
 Nicolas Tabareau <nicolas.tabareau@inria.fr>       nicolas tabareau <nicolas.tabareau@gmail.com>
+Nicolas Tabareau <nicolas.tabareau@inria.fr>       tabareau <tabareau@users.noreply.github.com>
 Enrico Tassi <Enrico.Tassi@inria.fr>               gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Enrico Tassi <Enrico.Tassi@inria.fr>               <Enrico.Tassi@inria.fr>
 Enrico Tassi <Enrico.Tassi@inria.fr>               Enrico Tassi <enrico.tassi@inria.fr>
@@ -248,6 +259,7 @@ Oliver Turner <aryaelfren@aryaelfren.eu>           Arya-Elfren <aryaelfren@aryae
 Quentin Vermande <quentin.vermande@orange.fr>      Quentin Vermande <quentin.vermande@orange.fr>
 Quentin Vermande <quentin.vermande@orange.fr>      qvermande <quentin.vermande@ens.psl.eu>
 Benjamin Werner <werner@gforge>                    werner <werner@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Théo Winterhalter < >                              TheoWinterhalter
 Li-yao Xia <lysxia@gmail.com>                      Lysxia <lysxia@gmail.com>
 Li-yao Xia <lysxia@gmail.com>                      Xia Li-yao <lysxia@gmail.com>
 Li-yao Xia <lysxia@gmail.com>                      Xia Li-yao <Lysxia@users.noreply.github.com>
@@ -262,6 +274,7 @@ Théo Zimmermann <theo.zimmermann@telecom-paris.fr> Théo Zimmermann <theo.zimme
 Théo Zimmermann <theo.zimmermann@telecom-paris.fr> Zimmi48 <theo.zimmermann@univ-paris-diderot.fr>
 Théo Zimmermann <theo.zimmermann@telecom-paris.fr> Zimmi48 <Zimmi48@users.noreply.github.com>
 Théo Zimmermann <theo.zimmermann@telecom-paris.fr> <Théo Zimmermann <theo.zimmermann@inria.fr>
+ypopovitch <yannick.popovitch2@gmail.com>          popitel <y@p.fr>
 
 # Anonymous accounts
 

Makefile

@@ -51,10 +51,10 @@ help:
 	@echo "  Note: these targets produce a developer build, not suitable"
 	@echo "        for distribution to end-users or install"
 	@echo ""
-	@echo " To run an \$$app \\in {coqc,coqtop,coqtop.byte,rocqide}:"
+	@echo " To run rocq:"
 	@echo ""
-	@echo "  - use 'dune exec -- dev/shim/\$$app args'"
-	@echo "    Example: 'dune exec -- dev/shim/coqc file.v'"
+	@echo "  - use 'dune exec -- rocq \$$subcommand args'"
+	@echo "    Example: 'dune exec -- rocq compile file.v'"
 	@echo ""
 	@echo " Documentation targets:"
 	@echo ""
@@ -158,8 +158,8 @@ DUNE_FILES=theories/Corelib/dune theories/Ltac2/dune
 
 dunestrap: $(DUNE_FILES)
 
-states: dunestrap
-	dune build $(DUNEOPT) dev/shim/coqtop
+states: world
+	echo "'make states' is an alias for 'make world'"
 
 MAIN_TARGETS:=rocq-runtime.install coq-core.install rocq-core.install \
   coqide-server.install rocq-devtools.install

README.md

@@ -1,20 +1,16 @@
 # The Rocq Prover
 
 [![GitLab CI][gitlab-badge]][gitlab-link]
-[![GitHub macOS CI][gh-macos-badge]][gh-macos-link]
-[![GitHub Windows CI][gh-win-badge]][gh-win-link]
+[![GitHub CI][gh-badge]][gh-link]
 [![Zulip][zulip-badge]][zulip-link]
 [![Discourse][discourse-badge]][discourse-link]
 [![DOI][doi-badge]][doi-link]
 
 [gitlab-badge]: https://gitlab.inria.fr/coq/coq/badges/master/pipeline.svg
 [gitlab-link]: https://gitlab.inria.fr/coq/coq/commits/master
 
-[gh-macos-badge]: https://github.com/rocq-prover/rocq/actions/workflows/ci-macos.yml/badge.svg
-[gh-macos-link]: https://github.com/rocq-prover/rocq/actions/workflows/ci-macos.yml
-
-[gh-win-badge]: https://github.com/rocq-prover/rocq/actions/workflows/ci-windows.yml/badge.svg
-[gh-win-link]: https://github.com/rocq-prover/rocq/actions/workflows/ci-windows.yml
+[gh-badge]: https://github.com/rocq-prover/rocq/actions/workflows/ci-github.yml/badge.svg
+[gh-link]: https://github.com/rocq-prover/rocq/actions/workflows/ci-github.yml
 
 [discourse-badge]: https://img.shields.io/badge/Discourse-forum-informational.svg
 [discourse-link]: https://discourse.rocq-prover.org/

boot/env.mli

@@ -136,3 +136,5 @@ val ocamlfind : unit -> string
 val print_config : ?prefix_var_name:string -> t -> out_channel -> unit
 
 val relocate : Coq_config.relocatable_path -> string
+
+val rocqbin : string

checker/safe_checking.ml

@@ -15,7 +15,9 @@ let import senv opac clib vmtab digest =
   let dp = Safe_typing.dirpath_of_library clib in
   let mb = Safe_typing.module_of_library clib in
   let env = Safe_typing.env_of_safe_env senv in
-  let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in
+  let qualities, univs = Safe_typing.univs_of_library clib in
+  let env = push_quality_set qualities env in
+  let env = push_context_set ~strict:true univs env in
   let env = Modops.add_retroknowledge (Mod_declarations.mod_retroknowledge mb) env in
   let env = Environ.link_vm_library vmtab env in
   let opac = Mod_checking.check_module env opac (Names.ModPath.MPfile dp) mb in

checker/values.ml

@@ -185,7 +185,10 @@ let v_level = v_tuple "level" [|v_int;v_raw_level|]
 let v_expr = v_tuple "levelexpr" [|v_level;v_int|]
 let v_univ = v_list v_expr
 
-let v_qvar = v_sum "qvar" 0 [|[|v_int|];[|v_string;v_int|]|]
+let v_qglobal = v_pair v_dp v_id
+
+(* perhaps the "Unif" constructor should be forbidden in vo files *)
+let v_qvar = v_sum "qvar" 0 [|[|v_int|];[|v_string;v_int|];[|v_qglobal|]|]
 
 let v_constant_quality = v_enum "constant_quality" 3
 
@@ -580,7 +583,7 @@ let v_vodigest = v_sum_c ("module_impl",0, [| [|v_string|]; [|v_string;v_string|
 let v_deps = v_array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_flags = v_tuple "flags" [|v_bool|] (* Allow Rewrite Rules *)
 let v_compiled_lib =
-  v_tuple "compiled" [|v_dp;v_module;v_context_set;v_set v_qvar;v_deps; v_flags|]
+  v_tuple "compiled" [|v_dp;v_module;v_pair (v_set v_qvar) v_context_set;v_deps; v_flags|]
 
 (** Toplevel structures in a vo (see Cic.mli) *)
 

coq-core.opam

@@ -16,7 +16,9 @@ Feit-Thompson theorem or homotopy type theory) and teaching.
 
 This package includes compatibility binaries to call Rocq
 through previous Coq commands like coqc coqtop,..."""
-maintainer: ["The Rocq development team <coqdev@inria.fr>"]
+maintainer: [
+  "The Rocq development team <rocq+rocq-development@discoursemail.com>"
+]
 authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://rocq-prover.org/"

coqide-server.opam

@@ -12,7 +12,9 @@ This package provides the `coqidetop` language server, an
 implementation of Rocq's [XML protocol](https://github.com/rocq-prover/rocq/blob/master/dev/doc/xml-protocol.md)
 which allows clients, such as RocqIDE, to interact with the Rocq Prover in a
 structured way."""
-maintainer: ["The Rocq development team <coqdev@inria.fr>"]
+maintainer: [
+  "The Rocq development team <rocq+rocq-development@discoursemail.com>"
+]
 authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://rocq-prover.org/"

coqpp/coqpp_main.ml

@@ -252,7 +252,7 @@ function
 | "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s
 | "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s
 | "NUMBER", None -> fprintf fmt "Tok.PNUMBER None"
-| "NUMBER", Some s -> fprintf fmt "Tok.PNUMBER (Some (NumTok.Unsigned.of_string %a))" print_string s
+| "NUMBER", Some s -> fprintf fmt "Tok.PNUMBER (Some (Option.get (NumTok.Unsigned.parse_string %a)))" print_string s
 | "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s
 | "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK"
 | "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s
@@ -369,9 +369,9 @@ let print_rule_classifier fmt r = match r.vernac_class with
 | Some f ->
   let no_binder = function ExtTerminal _ -> true | ExtNonTerminal _ -> false in
   if List.for_all no_binder r.vernac_toks then
-    fprintf fmt "Some @[%a@]" print_code f
+    fprintf fmt "Some @[(fun ~atts -> %a)@]" print_code f
   else
-    fprintf fmt "Some @[(fun %a-> %a)@]" print_binders r.vernac_toks print_code f
+    fprintf fmt "Some @[(fun %a ~atts -> %a)@]" print_binders r.vernac_toks print_code f
 
 (* let print_atts fmt = function *)
 (*   | None -> fprintf fmt "@[let () = Attributes.unsupported_attributes atts in@] " *)
@@ -477,13 +477,16 @@ let print_rules state fmt rules =
   print_list fmt (fun fmt r -> fprintf fmt "(%a)" (print_rule state) r) rules
 
 let print_classifier fmt = function
+(* error could be interesting but would need to check that not all of the rules have a classifier,
+   if we do that we could also check that at least 1 rule has no classifier
+   when the block level classifier is specified *)
 | ClassifDefault -> fprintf fmt ""
 | ClassifName "QUERY" ->
-  fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_query)"
+  fprintf fmt "~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_query)"
 | ClassifName "SIDEFF" ->
-  fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_sideeff)"
+  fprintf fmt "~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_sideeff)"
 | ClassifName s -> fatal (Printf.sprintf "Unknown classifier %s" s)
-| ClassifCode c -> fprintf fmt "~classifier:(%s)" c.code
+| ClassifCode c -> fprintf fmt "~classifier:(fun ~atts -> %s)" c.code
 
 let print_entry fmt = function
 | None -> fprintf fmt "None"