diff --git a/.github/workflows/check-conflicts.yml b/.github/workflows/check-conflicts.yml.disabled similarity index 100% rename from .github/workflows/check-conflicts.yml rename to .github/workflows/check-conflicts.yml.disabled diff --git a/.github/workflows/ci-github.yml b/.github/workflows/ci-github.yml.disabled similarity index 100% rename from .github/workflows/ci-github.yml rename to .github/workflows/ci-github.yml.disabled diff --git a/.github/workflows/sl-fm-ci.yml b/.github/workflows/sl-fm-ci.yml new file mode 100644 index 000000000000..1dc836281720 --- /dev/null +++ b/.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 diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml.disabled similarity index 100% rename from .github/workflows/stale.yml rename to .github/workflows/stale.yml.disabled diff --git a/.gitignore b/.gitignore index ebf7a66f5182..dd015461fac2 100644 --- a/.gitignore +++ b/.gitignore @@ -158,6 +158,4 @@ bin *.install .dune-stamp -/theories/Corelib/dune -/theories/Ltac2/dune /test-suite/test_suite_config.inc diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 239330edeb74..0259dd803a99 100644 --- a/.gitlab-ci.yml +++ b/.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" diff --git a/.mailmap b/.mailmap index 42765be094c1..433443935e31 100644 --- a/.mailmap +++ b/.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 blumer Guillaume Allais gallais Abhishek Anand Abhishek Anand (@brixpro-home) Abhishek Anand Abhishek Anand (optiplex7010@home) Léo Andrès zapashcanon +Florian Angeletti < > Octachron Jim Apple jbapple Bruno Barras barras Bruno Barras barras-local @@ -56,6 +58,8 @@ Juan Conejero Juan C corbinea Judicaël Courant courant Pierre Courtieu courtieu +Pierre Courtieu Matafou +Julien Cretin ia0 David Delahaye delahaye Maxime Dénès mdenes Maxime Dénès Maxime Denes @@ -71,6 +75,7 @@ Louise Dubois de Prisque < > louiseddp formalize.eth ilya Andres Erbsen Andres Erbsen Andres Erbsen andres-erbsen +Jian Fang Rw1nd Jim Fehrle Jim Jim Fehrle Jim Fehrle Jim Fehrle jfehrle @@ -133,6 +138,7 @@ Evgenii Kosogorov <284661@niuitmo.ru> doctor-kaliy Ethan A. Kuefner e kuefner Ambroise Lafont amblaf Ambroise Lafont Ambroise +Lucie Lahaye Lucie Thomas Lamiaux < > thomas-lamiaux Vincent Laporte Vincent Laporte Vincent Laporte Vincent Laporte @@ -143,6 +149,7 @@ William Lawvere william-lawvere llee454@gmail.com Larry Darryl Lee Jr. Larry D. Lee Jr Rodolphe Lepigre rlepigre +Rodolphe Lepigre rlepigre-skylabs-ai Xavier Leroy Xavier Leroy Pierre Letouzey letouzey Pierre Letouzey letouzey @@ -167,6 +174,7 @@ Erik Martin-Dorel Erik Martin-Dorel erikmd Julien Narboux jnarboux Julien Narboux narboux +Patrick Nicodemus < > patrick-nicodemus Jean-Marc Notin notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty Charles Norton CharlesCNorton <135471798+CharlesCNorton@users.noreply.github.com> Jean-Marc Notin notin @@ -203,11 +211,13 @@ Jean-Pierre Rodi Fourchaux Villetaneuse Pierre Roux Pierre Roux Pierre Roux proux01 +Radosław Rowicki radrow Matthew Ryan mrmr1993 Claudio Sacerdoti Coen sacerdot Kazuhiko Sakaguchi Kazuhiko Sakaguchi Kazuhiko Sakaguchi Kazuhiko Sakaguchi Kazuhiko Sakaguchi pi8027 +Gabriel Scherer < > gasche Marcello Seri Vincent Siles vsiles Kartik Singhal Kartik Singhal @@ -226,6 +236,7 @@ Paul Steckler Paul Steckler staffehn Sergei Stepanenko Kaptch Nicolas Tabareau nicolas tabareau +Nicolas Tabareau tabareau Enrico Tassi gareuselesinge Enrico Tassi Enrico Tassi Enrico Tassi @@ -248,6 +259,7 @@ Oliver Turner Arya-Elfren Quentin Vermande Quentin Vermande qvermande Benjamin Werner werner +Théo Winterhalter < > TheoWinterhalter Li-yao Xia Lysxia Li-yao Xia Xia Li-yao Li-yao Xia Xia Li-yao @@ -262,6 +274,7 @@ Théo Zimmermann Théo Zimmermann Zimmi48 Théo Zimmermann Zimmi48 Théo Zimmermann +ypopovitch popitel # Anonymous accounts diff --git a/Makefile b/Makefile index 3b02d5a5edfe..54eecf7f570a 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index be3cfe6d9f91..6b0844c88ec5 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,7 @@ # 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] @@ -10,11 +9,8 @@ [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/ diff --git a/boot/env.mli b/boot/env.mli index 1adf27b67b3c..08e58247d245 100644 --- a/boot/env.mli +++ b/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 diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml index 2a8a0486f1da..67ed74d66443 100644 --- a/checker/safe_checking.ml +++ b/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 diff --git a/checker/values.ml b/checker/values.ml index 65697d634e78..60b3be301e06 100644 --- a/checker/values.ml +++ b/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) *) diff --git a/coq-core.opam b/coq-core.opam index ffa2e1269dfc..4fcb035d73c3 100644 --- a/coq-core.opam +++ b/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 "] +maintainer: [ + "The Rocq development team " +] authors: ["The Rocq development team, INRIA, CNRS, and contributors"] license: "LGPL-2.1-only" homepage: "https://rocq-prover.org/" diff --git a/coqide-server.opam b/coqide-server.opam index 852fa3791bea..82a1809fe795 100644 --- a/coqide-server.opam +++ b/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 "] +maintainer: [ + "The Rocq development team " +] authors: ["The Rocq development team, INRIA, CNRS, and contributors"] license: "LGPL-2.1-only" homepage: "https://rocq-prover.org/" diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index e05948d5c459..280d2fff032e 100644 --- a/coqpp/coqpp_main.ml +++ b/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" diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 469e58e1c59c..bf303f2bb2ad 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -65,52 +65,52 @@ function subproject { ######################################################################## # MathComp ######################################################################## -project mathcomp "https://github.com/math-comp/math-comp" "master" +project mathcomp 'https://github.com/math-comp/math-comp' '0c8979a7a24cb71d5e986a66548d56d57f30762d' # Contact @CohenCyril, @proux01 on github -project fourcolor "https://github.com/math-comp/fourcolor" "master" +project fourcolor 'https://github.com/math-comp/fourcolor' 'dff565790a6aad4d64373046e723c4163c85b5f9' # Contact @ybertot, @proux01 on github -project oddorder "https://github.com/math-comp/odd-order" "master" +project oddorder 'https://github.com/math-comp/odd-order' '0ae93b443d14becaab819d1de490df88d5fb9d19' # Contact @gares, @proux01 on github -project mczify "https://github.com/math-comp/mczify" "master" +project mczify 'https://github.com/math-comp/mczify' 'd4ec06f83fdadaac59734557803094a3cd63f3d0' # Contact @pi8027 on github -project algebra_tactics "https://github.com/math-comp/algebra-tactics" "master" +project algebra_tactics 'https://github.com/math-comp/algebra-tactics' '9d17d45cadc4d0a3ca971c8b4e13bf5db2bff26a' # Contact @pi8027, @proux01 on github -project finmap "https://github.com/math-comp/finmap" "master" +project finmap 'https://github.com/math-comp/finmap' '054881ad521ab62d9fd3457ba541a3d4f3734147' # Contact @CohenCyril on github -project bigenough "https://github.com/math-comp/bigenough" "master" +project bigenough 'https://github.com/math-comp/bigenough' '596834243018593f1855201d2ff7228d09f1afde' # Contact @CohenCyril on github -project analysis "https://github.com/math-comp/analysis" "master" +project analysis 'https://github.com/math-comp/analysis' '6e62b37d02cb8fd357a054a91c160e07671a7d40' # Contact @affeldt-aist, @CohenCyril on github ######################################################################## # UniMath ######################################################################## -project unimath "https://github.com/UniMath/UniMath" "master" +project unimath 'https://github.com/UniMath/UniMath' '5941f44e3c13d2ac385f5a8b9b486c0088dd3f46' # Contact @benediktahrens, @m-lindgren, @nmvdw, @rmatthes on github ######################################################################## # Unicoq + Mtac2 ######################################################################## -project unicoq "https://github.com/unicoq/unicoq" "master" +project unicoq 'https://github.com/unicoq/unicoq' '28ec18aef35877829535316fc09825a25be8edf1' # Contact @beta-ziliani, @Janno, @mattam82 on github -project mtac2 "https://github.com/Mtac2/Mtac2" "master" +project mtac2 'https://github.com/Mtac2/Mtac2' 'bcbefa79406fc113f878eb5f89758de241d81433' # Contact @beta-ziliani, @Janno, @mattam82 on github ######################################################################## # Mathclasses + Corn ######################################################################## -project math_classes "https://github.com/coq-community/math-classes" "master" +project math_classes 'https://github.com/coq-community/math-classes' '40de430909768abae6ed34be818ecfad809342e3' # Contact @Lysxia and @spitters on github -project corn "https://github.com/coq-community/corn" "master" +project corn 'https://github.com/coq-community/corn' '138bc18c32561b03f184c5cc2ab2ed7a7f363d78' # Contact @Lysxia and @spitters on github ######################################################################## @@ -128,88 +128,88 @@ project stdpp "https://gitlab.mpi-sws.org/iris/stdpp" "" project iris "https://gitlab.mpi-sws.org/iris/iris" "" # Contact @RalfJung, @robbertkrebbers on github -project autosubst "https://github.com/coq-community/autosubst" "master" +project autosubst 'https://github.com/coq-community/autosubst' '50dfe574c0bd415925eea47c1f5b1a533aa85269' # Contact @RalfJung, @co-dan on github -project iris_examples "https://gitlab.mpi-sws.org/iris/examples" "master" +project iris_examples 'https://gitlab.mpi-sws.org/iris/examples' 'dc20f8669b503db47030223dcf465b26577cb34a' # Contact @RalfJung, @robbertkrebbers on github ######################################################################## # HoTT ######################################################################## -project hott "https://github.com/HoTT/HoTT" "master" +project hott 'https://github.com/HoTT/HoTT' 'de76def86967866f7ca9cc3f3c17b40f2ab16bb1' # Contact @Alizter, @jdchristensen on github ######################################################################## # CoqHammer ######################################################################## -project coqhammer "https://github.com/lukaszcz/coqhammer" "master" +project coqhammer 'https://github.com/lukaszcz/coqhammer' '8649603dcbac5d92eaf1319a6b7cdfc65cdd804b' # Contact @lukaszcz on github ######################################################################## # Flocq ######################################################################## -project flocq "https://gitlab.inria.fr/flocq/flocq" "master" +project flocq 'https://gitlab.inria.fr/flocq/flocq' 'd0875fdba19cb4689cf1de6164d0adfd6b5e9d75' # Contact @silene on github ######################################################################## # coq-performance-tests ######################################################################## -project coq_performance_tests "https://github.com/coq-community/coq-performance-tests" "master" +project coq_performance_tests 'https://github.com/coq-community/coq-performance-tests' '940baa2bc2753ba65d2c9d0918618aa50721902c' # Contact @JasonGross on github ######################################################################## # coq-tools ######################################################################## -project coq_tools "https://github.com/JasonGross/coq-tools" "master" +project coq_tools 'https://github.com/JasonGross/coq-tools' '2d9bb862ec97979ad25cb1a000a6c7c2f38928fd' # Contact @JasonGross on github ######################################################################## # Coquelicot ######################################################################## -project coquelicot "https://gitlab.inria.fr/coquelicot/coquelicot" "master" +project coquelicot 'https://gitlab.inria.fr/coquelicot/coquelicot' 'dbcd5010d1770eb8cd3bf100a0a2f51acaa6b661' # Contact @silene on github ######################################################################## # CompCert ######################################################################## -project compcert "https://github.com/AbsInt/CompCert" "master" +project compcert 'https://github.com/AbsInt/CompCert' '76f7feabd0d549a12ca139d6af953c4c30e814cc' # Contact @xavierleroy on github ######################################################################## # VST ######################################################################## -project vst "https://github.com/PrincetonUniversity/VST" "master" +project vst 'https://github.com/PrincetonUniversity/VST' '127aa7346e1dbd8da066a2a11c540ee6768a485b' # Contact @andrew-appel on github ######################################################################## # cross-crypto ######################################################################## -project cross_crypto "https://github.com/mit-plv/cross-crypto" "master" +project cross_crypto 'https://github.com/mit-plv/cross-crypto' 'a99fefcf4310264c178cd53d731af97c0f1c82f9' # Contact @andres-erbsen on github ######################################################################## # rewriter ######################################################################## -project rewriter "https://github.com/mit-plv/rewriter" "master" +project rewriter 'https://github.com/mit-plv/rewriter' '9496defb8b236f442d11372f6e0b5e48aa38acfc' # Contact @JasonGross on github ######################################################################## # fiat_parsers ######################################################################## -project fiat_parsers "https://github.com/mit-plv/fiat" "master" +project fiat_parsers 'https://github.com/mit-plv/fiat' 'd6f2f59fa6a6ebbb5cff818bab8c3f1f16fea1bd' # Contact @JasonGross on github ######################################################################## # fiat_crypto_legacy ######################################################################## -project fiat_crypto_legacy "https://github.com/mit-plv/fiat-crypto" "sp2019latest" +project fiat_crypto_legacy 'https://github.com/mit-plv/fiat-crypto' '54d90a996f4155d985df3fd126c3c242e35342b9' # Contact @JasonGross on github ######################################################################## # fiat_crypto ######################################################################## -project fiat_crypto "https://github.com/mit-plv/fiat-crypto" "master" +project fiat_crypto 'https://github.com/mit-plv/fiat-crypto' '9eb8af1324ad20332042987900fecbb33b048803' # Contact @andres-erbsen, @JasonGross on github # bedrock2, coqutil, rupicola, kami, riscv_coq @@ -226,221 +226,221 @@ subproject riscv_coq bedrock2 "deps/riscv-coq" "https://github.com/mit-plv/riscv ######################################################################## # coq_dpdgraph ######################################################################## -project coq_dpdgraph "https://github.com/coq-community/coq-dpdgraph" "coq-master" +project coq_dpdgraph 'https://github.com/coq-community/coq-dpdgraph' '7817def06d4e3abc2e54a2600cf6e29d63d58b8a' # Contact @Karmaki, @ybertot on github ######################################################################## # CoLoR ######################################################################## -project color "https://github.com/fblanqui/color" "master" +project color 'https://github.com/fblanqui/color' '7ef5cf16c45421283445f999787886479a3a8746' # Contact @fblanqui on github ######################################################################## # TLC ######################################################################## -project tlc "https://github.com/charguer/tlc" "master-for-coq-ci" +project tlc 'https://github.com/charguer/tlc' '51be762eedec72788490f1fd222eb8b0d82b8bea' # Contact @charguer on github ######################################################################## # Bignums ######################################################################## -project bignums "https://github.com/coq/bignums" "master" +project bignums 'https://github.com/coq/bignums' '9f9855536bd4167af6986f826819e32354b7da22' # Contact @erikmd, @proux01 on github ######################################################################## # coqprime ######################################################################## -project coqprime "https://github.com/thery/coqprime" "master" +project coqprime 'https://github.com/thery/coqprime' '45c784d122ed84194cd977c8453c98acd529193f' # Contact @thery on github ######################################################################## # bbv ######################################################################## -project bbv "https://github.com/mit-plv/bbv" "master" +project bbv 'https://github.com/mit-plv/bbv' 'c53d5b95c70839ae8e947010d85503bd1ada1120' # Contact @JasonGross, @samuelgruetter on github ######################################################################## # Coinduction ######################################################################## -project coinduction "https://github.com/damien-pous/coinduction" "master" +project coinduction 'https://github.com/damien-pous/coinduction' '823b424778feff8fbd9759bc3a044435ea4902d1' # Contact @damien-pous on github ######################################################################## # coq-lsp ######################################################################## -project coq_lsp "https://github.com/ejgallego/coq-lsp" "main" +project coq_lsp 'https://github.com/ejgallego/coq-lsp' 'a46cd5f97e072ccb2977cd8efa152076a14c52fc' # Contact @ejgallego on github ######################################################################## # Equations ######################################################################## -project equations "https://github.com/mattam82/Coq-Equations" "main" +project equations 'https://github.com/mattam82/Coq-Equations' '2137c8e7081f2d47ab903de0cc09fd6a05bfab01' # Contact @mattam82 on github ######################################################################## # Elpi + Hierarchy Builder ######################################################################## -project elpi "https://github.com/LPCIC/coq-elpi" "master" +project elpi 'https://github.com/LPCIC/coq-elpi' '157bd2af292d1a0f58741bf2d037eb3d1480e26b' # Contact @gares on github -project hierarchy_builder "https://github.com/math-comp/hierarchy-builder" "master" +project hierarchy_builder 'https://github.com/math-comp/hierarchy-builder' '4b6a76fb6802a770dd929a9dd7e8e03c3a47f73e' # Contact @CohenCyril, @gares on github ######################################################################## # Engine-Bench ######################################################################## -project engine_bench "https://github.com/mit-plv/engine-bench" "master" +project engine_bench 'https://github.com/mit-plv/engine-bench' '08ecd3ae6e73ff6e62b47fd62f5c57e4ec4fb42d' # Contact @JasonGross on github ######################################################################## # fcsl-pcm ######################################################################## -project fcsl_pcm "https://github.com/imdea-software/fcsl-pcm" "master" +project fcsl_pcm 'https://github.com/imdea-software/fcsl-pcm' '69c244e93e6790100065eb59a307adba6d1775a8' # Contact @aleksnanevski, @clayrat on github ######################################################################## # ext-lib ######################################################################## -project ext_lib "https://github.com/coq-community/coq-ext-lib" "master" +project ext_lib 'https://github.com/coq-community/coq-ext-lib' 'b27e806daf39a8f1cfc7ced09c1af44d390af4a6' # Contact @gmalecha, @liyishuai on github ######################################################################## # simple-io ######################################################################## -project simple_io "https://github.com/Lysxia/coq-simple-io" "master" +project simple_io 'https://github.com/Lysxia/coq-simple-io' '98d038bba0a481deb1bd03c3e05c5abd5d48be73' # Contact @Lysxia, @liyishuai on github ######################################################################## # quickchick ######################################################################## -project quickchick "https://github.com/QuickChick/QuickChick" "master" +project quickchick 'https://github.com/QuickChick/QuickChick' '29ef41e628319e4d39dea377ffa49dd541705869' # Contact @lemonidas, @Lysxia, @liyishuai on github ######################################################################## # reduction-effects ######################################################################## -project reduction_effects "https://github.com/coq-community/reduction-effects" "master" +project reduction_effects 'https://github.com/coq-community/reduction-effects' '2e6590125885906ec0c5157b114d2afba18ab9c8' # Contact @liyishuai, @JasonGross on github ######################################################################## # menhirlib ######################################################################## # Note: menhirlib is now in subfolder coq-menhirlib of menhir -project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "master" +project menhirlib 'https://gitlab.inria.fr/fpottier/menhir' 'ac08b55d316e6814d4bda1c995e7e0ed008c0e76' # Contact @fpottier, @jhjourdan on github ######################################################################## # coq-neural-net-interp ######################################################################## -project neural_net_interp "https://github.com/JasonGross/neural-net-coq-interp" "tested" +project neural_net_interp 'https://github.com/JasonGross/neural-net-coq-interp' '7e0c38173eb9147bde15e17ac43583df96289465' # Contact @JasonGross on github ######################################################################## # aac_tactics ######################################################################## -project aac_tactics "https://github.com/coq-community/aac-tactics" "master" +project aac_tactics 'https://github.com/coq-community/aac-tactics' 'e68d028cef838f5821d184fed0caea9eedd5538a' # Contact @palmskog on github ######################################################################## # paco ######################################################################## -project paco "https://github.com/snu-sf/paco" "master" +project paco 'https://github.com/snu-sf/paco' 'd0561bf7f0a96cac486ba3bd8ca0b72ce01fb9cf' # Contact @minkiminki on github ######################################################################## # coq-itree ######################################################################## -project itree "https://github.com/DeepSpec/InteractionTrees" "master" +project itree 'https://github.com/DeepSpec/InteractionTrees' 'cf1443c88aca8691d93ce84fc633145752e7944e' # Contact @Lysxia on github ######################################################################## # coq-itree_io ######################################################################## -project itree_io "https://github.com/Lysxia/coq-itree-io" "master" +project itree_io 'https://github.com/Lysxia/coq-itree-io' 'af0326793a19f142eba800dba6044143b108ceaa' # Contact @Lysxia, @liyishuai on github ######################################################################## # coq-ceres ######################################################################## -project ceres "https://github.com/Lysxia/coq-ceres" "master" +project ceres 'https://github.com/Lysxia/coq-ceres' 'f61b24d48222db0100de19f88c19151a3aeb826f' # Contact @Lysxia on github ######################################################################## # coq-parsec ######################################################################## -project parsec "https://github.com/liyishuai/coq-parsec" "master" +project parsec 'https://github.com/liyishuai/coq-parsec' '3feabc998705927ca2d2f9249a21a6e15c394162' # Contact @liyishuai on github ######################################################################## # coq-json ######################################################################## -project json "https://github.com/liyishuai/coq-json" "master" +project json 'https://github.com/liyishuai/coq-json' '8069b6b4d544ea3011246dfa04d2c1c550d50455' # Contact @liyishuai on github ######################################################################## # coq-async-test ######################################################################## -project async_test "https://github.com/liyishuai/coq-async-test" "master" +project async_test 'https://github.com/liyishuai/coq-async-test' '0637b95ae52060d8a808261ca97890d03c9a4503' # Contact @liyishuai on github ######################################################################## # coq-http ######################################################################## -project http "https://github.com/liyishuai/coq-http" "master" +project http 'https://github.com/liyishuai/coq-http' 'cabde79a4a0d978d031475c7443be7fd43a711c5' # Contact @liyishuai on github ######################################################################## # paramcoq ######################################################################## -project paramcoq "https://github.com/coq-community/paramcoq" "master" +project paramcoq 'https://github.com/coq-community/paramcoq' '937537d416bc5f7b81937d4223d7783d0e687239' # Contact @ppedrot on github ######################################################################## # relation_algebra ######################################################################## -project relation_algebra "https://github.com/damien-pous/relation-algebra" "master" +project relation_algebra 'https://github.com/damien-pous/relation-algebra' '4db15229396abfd8913685be5ffda4f0fdb593d9' # Contact @damien-pous on github ######################################################################## # StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft ######################################################################## -project struct_tact "https://github.com/uwplse/StructTact" "master" +project struct_tact 'https://github.com/uwplse/StructTact' '97268e11564c8fe59aa72b062478458d7aa53e9d' # Contact @palmskog on github -project inf_seq_ext "https://github.com/DistributedComponents/InfSeqExt" "master" +project inf_seq_ext 'https://github.com/DistributedComponents/InfSeqExt' '601e89ec019501c48c27fcfc14b9a3c70456e408' # Contact @palmskog on github -project cheerios "https://github.com/uwplse/cheerios" "master" +project cheerios 'https://github.com/uwplse/cheerios' '5c9318c269f9cae1c1c6583a44405969ac0be0dd' # Contact @palmskog on github -project verdi "https://github.com/uwplse/verdi" "master" +project verdi 'https://github.com/uwplse/verdi' 'b7f77848819878b1faf0e2e6a730f9bb850130be' # Contact @palmskog on github -project verdi_raft "https://github.com/uwplse/verdi-raft" "master" +project verdi_raft 'https://github.com/uwplse/verdi-raft' 'a3375e867326a82225e724cc1a7b4758b029376f' # Contact @palmskog on github ######################################################################## # Stdlib ######################################################################## -project stdlib "https://github.com/coq/stdlib" "master" +project stdlib 'https://github.com/coq/stdlib' '2b23d2d3b313d5fe8b54a649a4aca6977a144648' # Contact TODO on github ######################################################################## # argosy ######################################################################## -project argosy "https://github.com/mit-pdos/argosy" "master" +project argosy 'https://github.com/mit-pdos/argosy' '9fa42b78b7f9b7b989fb3434dfbfec4abcfcbff8' # Contact @tchajed on github ######################################################################## # ATBR ######################################################################## -project atbr "https://github.com/coq-community/atbr" "master" +project atbr 'https://github.com/coq-community/atbr' '47ac8fb6bf244d9a4049e04c01e561191490f543' # Contact @palmskog, @tchajed on github ######################################################################## # perennial ######################################################################## -project perennial "https://github.com/mit-pdos/perennial" "coq/tested" +project perennial 'https://github.com/mit-pdos/perennial' 'b39e2c342ba3da95e11a7db31c7be20560e92cae' # Contact @upamanyus, @RalfJung, @tchajed on github # PRs to fix Perennial failures should be submitted against the Perennial # `master` branch. `coq/tested` is automatically updated every night to the @@ -450,104 +450,104 @@ project perennial "https://github.com/mit-pdos/perennial" "coq/tested" ######################################################################## # metarocq ######################################################################## -project metarocq "https://github.com/MetaRocq/metarocq" "main" +project metarocq 'https://github.com/MetaRocq/metarocq' '2995003b88f3812e5649cfdd0f9a4c44ceaf0700' # Contact @mattam82, @yforster on github ######################################################################## # SF suite ######################################################################## -project sf "https://github.com/DeepSpec/sf" "master" +project sf 'https://github.com/DeepSpec/sf' '5e863a9f92e515a0e11641f28077a64919f8482e' # Contact @bcpierce00, @liyishuai on github ######################################################################## # Coqtail ######################################################################## -project coqtail "https://github.com/whonore/Coqtail" "main" +project coqtail 'https://github.com/whonore/Coqtail' '28340858a528a6e86d3eee2ff5ccbf56f3eaf43f' # Contact @whonore on github ######################################################################## # Deriving ######################################################################## -project deriving "https://github.com/arthuraa/deriving" "master" +project deriving 'https://github.com/arthuraa/deriving' '04105e8303199e588e0074e28123fd86c8c420f7' # Contact @arthuraa on github ######################################################################## # VsRocq ######################################################################## -project vsrocq "https://github.com/rocq-prover/vsrocq" "main" +project vsrocq 'https://github.com/rocq-prover/vsrocq' '93560217d1fa5c2b473718703007bd292719c2fc' # Contact @rtetley, @gares on github ######################################################################## # category-theory ######################################################################## -project category_theory "https://github.com/jwiegley/category-theory" "master" +project category_theory 'https://github.com/jwiegley/category-theory' '42684ff22decc06afeb4caeb31249b1e498cb1ce' # Contact @jwiegley on github ######################################################################## # itauto ######################################################################## -project itauto "https://gitlab.inria.fr/fbesson/itauto" "master" +project itauto 'https://gitlab.inria.fr/fbesson/itauto' 'ff11a568d000b94965a33de428c6e6700b920198' # Contact @fajb on github ######################################################################## # Mathcomp-word ######################################################################## -project mathcomp_word "https://github.com/jasmin-lang/coqword" "main" +project mathcomp_word 'https://github.com/jasmin-lang/coqword' 'a34107995570598dd3844b530924db83e1c82932' # Contact @vbgl, @strub on github ######################################################################## # Jasmin ######################################################################## -project jasmin "https://github.com/jasmin-lang/jasmin" "main" +project jasmin 'https://github.com/jasmin-lang/jasmin' 'c8188deeedf67e7633b4fbda4aacb13da14cba61' # Contact @vbgl, @bgregoir on github ######################################################################## # Lean Importer ######################################################################## -project lean_importer "https://github.com/coq-community/rocq-lean-import" "master" +project lean_importer 'https://github.com/coq-community/rocq-lean-import' 'c3546102f242aaa1e9af921c78bdb1132522e444' # Contact @SkySkimmer on github ######################################################################## # SMTCoq ######################################################################## -project smtcoq "https://github.com/smtcoq/smtcoq" "coq-master" +project smtcoq 'https://github.com/smtcoq/smtcoq' '5c6033c906249fcf98a48b4112f6996053124514' # Contact @ckeller on github -project smtcoq_trakt "https://github.com/smtcoq/smtcoq" "with-trakt-coq-master" +project smtcoq_trakt 'https://github.com/smtcoq/smtcoq' '9392f7446a174b770110445c155a07b183cdca3d' # Contact @ckeller on github ######################################################################## # Stalmarck ######################################################################## -project stalmarck "https://github.com/coq-community/stalmarck" "master" +project stalmarck 'https://github.com/coq-community/stalmarck' 'd32acd3c477c57b48dd92bdd96d53fb8fa628512' # Contact @palmskog on github ######################################################################## # Tactician ######################################################################## -project tactician "https://github.com/coq-tactician/coq-tactician" "coqdev" +project tactician 'https://github.com/coq-tactician/coq-tactician' '3a74c377ac9409d425f11f679eff7a34eaa5a45a' # Contact @LasseBlaauwbroek on github ######################################################################## # Ltac2 compiler ######################################################################## -project ltac2_compiler "https://github.com/SkySkimmer/coq-ltac2-compiler" "main" +project ltac2_compiler 'https://github.com/SkySkimmer/coq-ltac2-compiler' '2ee3660aad17b0310c07bab6ce94efdd45b67212' # Contact @SkySkimmer on github ######################################################################## # Waterproof ######################################################################## -project waterproof "https://github.com/impermeable/coq-waterproof" "coq-master" +project waterproof 'https://github.com/impermeable/coq-waterproof' 'dd712eb0b7f5c205870dbd156736a684d40eeb9a' # Contact @jellooo038, @jim-portegies on github ######################################################################## # Autosubst (2) OCaml ######################################################################## -project autosubst_ocaml "https://github.com/uds-psl/autosubst-ocaml" "master" +project autosubst_ocaml 'https://github.com/uds-psl/autosubst-ocaml' 'a4e154fb548197572326167809a4c612a2ec71ac' # Contact @yforster on github ######################################################################## # Trakt ######################################################################## -project trakt "https://github.com/ecranceMERCE/trakt" "coq-master" +project trakt 'https://github.com/ecranceMERCE/trakt' '956e78ab3680d186d03d8b58dbd90681174f3157' # Contact @ckeller, @louiseddp on github diff --git a/dev/ci/user-overlays/20738-SkySkimmer-improve-fixpoint-no-elim.sh b/dev/ci/user-overlays/20738-SkySkimmer-improve-fixpoint-no-elim.sh new file mode 100644 index 000000000000..2ad84f7511d0 --- /dev/null +++ b/dev/ci/user-overlays/20738-SkySkimmer-improve-fixpoint-no-elim.sh @@ -0,0 +1 @@ +overlay stdlib https://github.com/SkySkimmer/stdlib improve-fixpoint-no-elim 20738 diff --git a/dev/doc/README.md b/dev/doc/README.md index 4500e434033e..f2d9f2e5fa2e 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -55,17 +55,21 @@ $ make # to get an idea of the available targets $ make check # build all OCaml files as fast as possible -$ dune exec -- dev/shim/coqc-prelude test.v - # update coqc and the prelude and compile file test.v $ make world # build coq and the complete stdlib and setup it for use under _build/install/default # In particular, you may run, e.g., coq_makefile from _build/install/default # to build some test project +$ dune exec -- rocq test.v + # compile file test.v + # The "rocq" shim will be updated if needed, + # but not the worker binary and not the corelib .vo files ``` -When running the commands above, you may set `DUNEOPT=--display=short` -for a more verbose build (not required if you have already set the -default verbosity globally as described in the previous section). +When running the `make` targets above, you may set +`DUNEOPT=--display=short` for a more verbose build +(and use eg `dune exec --display=short -- rocq test.v` when calling dune directly) +(not required if you have already set the default verbosity globally +as described in the previous section). To learn how to run the test suite, you can read [`test-suite/README.md`](../../test-suite/README.md). diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index bb6678c4ae70..a74d4daf2158 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -27,10 +27,9 @@ For more targeted builds, you can also call `dune` directly. First, call `make dunestrap` to generate necessary build files (the `make` targets above do it automatically). Then you can use: -- `dune exec -- dev/shim/coqtop` : build and launch coqtop + prelude - [equivalent to `make states`]. -- `dune exec -- dev/shim/coqc `: build and launch `coqc` with - arguments of your choice +- `dune exec -- rocq `: + build and launch rocq (does not build the worker and Prelude.vo). + with arguments of your choice - `dune build $target`: where `$target` can refer to the build directory or the source directory [but will be placed under `_build`] @@ -106,31 +105,35 @@ Dune will read the file `~/.config/dune/config`; see `man dune-config`. Among others, you can set in this file the custom number of build threads `(jobs N)` and display options `(display _mode_)`. -## Running binaries [coqtop / rocqide] +## Running binaries (rocq compile, rocq top) -Running `coqtop` directly with `dune exec -- coqtop` won't in general -work well unless you are using `dune exec -- coqtop -noinit`. The -`coqtop` binary doesn't depend itself on Rocq's prelude, so plugins / -vo files may go stale if you rebuild only `coqtop`. +You should generally run `make world` before running rocq so that the +corelib is built and placed in `_build/install`. -Instead, you should use the provided "shims" for running `coqtop` and -`rocqide` in a fast build. In order to use them, do: +If building the corelib produces an error outside the prelude, `make +world` will still result in a usable state (of course you won't be +able to Require any failed files). -``` -$ dune exec -- dev/shim/coqtop -``` - -or `quickide` / `dev/shim/rocqide` for RocqIDE, etc.... See `dev/shim/dune` for a -complete list of targets. These targets enjoy quick incremental compilation -thanks to `-opaque` so they tend to be very fast while developing. +For errors inside the prelude, invoke rocq with +`-boot -noinit -R _build/default/theories/Corelib Corelib`. +For instance if you get an error in Datatypes, +~~~bash +dune exec -- rocq compile -boot -noinit -R _build/default/theories/Corelib Corelib _build/default/theories/Corelib/Init/Datatypes.v +~~~ +should reproduce it. -Note that for a fast developer build of ML files, the `check` target -is faster, as it doesn't link the binaries and uses the non-optimizing -compiler. +~~~bash +dune exec -- rocq compile -boot -noinit -R _build/default/theories/Corelib Corelib -R theories/Corelib Corelib theories/Corelib/Init/Datatypes.v +~~~ +should be equivalent. -If you built the full core library with the `world` target, -then you can run the commands in the -`_build/install/default/bin` directories (including `coq_makefile`). +Giving `-boot -R _build/default/theories/Corelib Corelib` to +an IDE while visiting a file in `theories/Corelib/Init` should combine with +`theories/Corelib/Init/_CoqProject` to produce the above result, eg +~~~bash +dune exec -- rocqide -boot -R _build/default/theories/Corelib Corelib theories/Corelib/Init/Datatypes.v +~~~ +should work to reproduce the error interactively. ## Building custom toplevels @@ -239,9 +242,9 @@ For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. ## Dropping from coqtop: -The following commands should work: +The following should work: ``` -dune exec -- dev/shim/coqtop.byte +dune exec -- rocq repl-with-drop > Drop. ``` diff --git a/dev/doc/critical-bugs.md b/dev/doc/critical-bugs.md index 5c05a6ce18de..c18aec6b863f 100644 --- a/dev/doc/critical-bugs.md +++ b/dev/doc/critical-bugs.md @@ -31,6 +31,7 @@ This file recollects knowledge about critical bugs found in Coq since version 8. - [module subtyping disrespected squashing status of inductives](#module-subtyping-disrespected-squashing-status-of-inductives) - [Functor inlining drops universe substitution](#functor-inlining-drops-universe-substitution) - [Primitives are incorrectly considered convertible to anything by module subtyping](#primitives-are-incorrectly-considered-convertible-to-anything-by-module-subtyping) + - [missing substitution when strengthening functors](#missing-substitution-when-strengthening-functors) - [Universes](#universes) - [issue with two parameters in the same universe level](#issue-with-two-parameters-in-the-same-universe-level) - [universe polymorphism can capture global universes](#universe-polymorphism-can-capture-global-universes) @@ -74,6 +75,7 @@ This file recollects knowledge about critical bugs found in Coq since version 8. - [Incorrect specification of PrimFloat.leb](#incorrect-specification-of-primfloatleb) - [Incorrect implementation of SFclassify.](#incorrect-implementation-of-sfclassify) - [nativenorm reading back closures as arbitrary floating-point values](#nativenorm-reading-back-closures-as-arbitrary-floating-point-values) + - [guard condition issue made it inconsistent with univalence](#guard-condition-issue-made-it-inconsistent-with-univalence) - [Deserialization](#deserialization) - [deserialization of .vo data not properly checked](#deserialization-of-vo-data-not-properly-checked) - [Probably non exploitable fixed bugs](#probably-non-exploitable-fixed-bugs) @@ -331,6 +333,18 @@ and lack of checking of relevance marks on constants in coqchk - exploit: see issue - risk: high if there is a Primitive in a Module Type, otherwise low +#### Missing substitution when strengthening functors + +- component: modules +- introduced: 8.5 for the kernel (c5b699f), 8.10 for the checker (#8773) +- impacted released versions: 8.5-9.0.0 +- impacted coqchk version: 8.10-9.0.0 +- fixed in: V9.0.1 +- found by: Pierre-Marie Pédrot +- GH issue number: rocq-prover/rocq#21051 +- exploit: see issue +- risk: could be exploited by mistake when using heavy module machinery + ### Universes #### issue with two parameters in the same universe level @@ -820,6 +834,18 @@ For instance `α` and `__U03b1_` were the same in the native compiler. - GH issue number: coq/coq#17871 - risk: proof of false when using primitive floats and native_compute +#### guard condition issue made it inconsistent with univalence + +- component: guard condition +- introduced: variant of [the issue with propositional extensionality](#guard-condition-was-unknown-to-be-inconsistent-with-propositional-extensionality-in-library-Sets) that was not fixed then +- impacted released versions: the relative inconsistency was present from the very beginning, until 9.0 +- impacted coqchk versions: *-9.0 +- fixed in: 9.0.1 +- fixed by further constraining the guard condition: [PR 21050](https://github.com/rocq-prover/rocq/pull/21050) +- found by: Thomas Lamiaux, Yann Leray, Pierre-Marie Pédrot, Nicolas Tabareau +- GH issue number: [21053](https://github.com/rocq-prover/issues/21053) +- risk: unlikely to be exploited by chance (?) + ### Deserialization #### deserialization of .vo data not properly checked diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index 49237a448c5f..7ba657009e53 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -1,7 +1,7 @@ Debugging from Rocq toplevel using OCaml toplevel ====================================================== -1. Launch bytecode version of Rocq (`dune exec -- dev/shim/coqtop.byte`) +1. Launch bytecode version of Rocq (`dune exec -- rocq repl-with-drop`) 2. Access OCaml toplevel using vernacular command `Drop.` 3. Use `#trace` to tell which function(s) to trace, or type any other OCaml toplevel commands or OCaml expressions diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md index 652c72bc6539..78957432fbc6 100644 --- a/dev/doc/parsing.md +++ b/dev/doc/parsing.md @@ -28,6 +28,7 @@ Notable attributes of the parser include: ## Contents ## +- [Vocabulary](#vocabulary) - [Grammars: `*.mlg` File Structure](#grammars-mlg-file-structure) - [Grammars: Nonterminals and Productions](#grammars-nonterminals-and-productions) - [Alternate production syntax](#alternate-production-syntax) @@ -36,10 +37,22 @@ Notable attributes of the parser include: - [Parsing productions](#parsing-productions) - [Lookahead](#lookahead) +## Vocabulary + +- *entry*: a nonterminal. Entries are values of type + `'a Procq.Entry.t` (`Entry.t` in the rest of this document), + where `'a` is the type of the parsed value. + For instance `Procq.Prim.qualid : qualid Entry.t` parses qualified identifiers ("qualid"). + +- *argument*: a nonterminal with associated functions (e.g. how to + print its values). Arguments are values of type + `('raw,'glb,'top) Genarg.genarg_type`, typically named `wit_foo`, + with an associated entry of type `'raw Entry.t` typically named `foo`. + ## Grammars: `*.mlg` File Structure ## -Grammars are defined in `*.mlg` files, which `coqpp` compiles into `*.ml` files at build time. -`coqpp` code is in the `coqpp` directory. `coqpp` uses yacc and lex to parse the grammar files. +Grammars are defined in `*.mlg` files, which `rocq preprocess-mlg` compiles into `*.ml` files at build time. +`preprocess-mlg` code is in the `coqpp` directory. `coqpp` uses yacc and lex to parse the grammar files. You can examine its yacc and lex input files in `coqpp_lex.mll` and `coqpp_parse.mly` for details not fully covered here. @@ -53,111 +66,252 @@ which has the full grammar for Rocq in one file and the parser action routines and other OCaml code are omitted. `*.mlg` files contain the following types of nodes (See `node` in the yacc grammar). This part is -very specific to Rocq (not so similar to Camlp5): - -* OCaml code - OCaml code enclosed in curly braces, which is copied verbatim to the generated `*.ml` file - -* Comments - comments in the `*.mlg` file in the form `(* … *)`, which are not copied - to the generated `*.ml` file. Comments in OCaml code are preserved. - -* `DECLARE_PLUGIN "*_plugin"` - associates the file with a specific plugin, for example "ltac_plugin" - -* `GRAMMAR EXTEND` - adds additional nonterminals and productions to the grammar and declares global - nonterminals referenced in the `GRAMMAR EXTEND`: - - ``` - GRAMMAR EXTEND Gram - GLOBAL: - bignat bigint …; - - END - ``` - - Global nonterminals are declared in `pcoq.ml`, e.g. `let bignat = Entry.create "bignat"`. - All the `*.mlg` files include `open Pcoq` and often its modules, e.g. `open Procq.Prim`. - - `GRAMMAR EXTEND` should be used only for large syntax additions. To add new commands - and tactics, use these instead: - - - `VERNAC COMMAND EXTEND` to add new commands - - `TACTIC EXTEND` to add new tactics - - `ARGUMENT EXTEND` to add new nonterminals - - These constructs provide essential semantic information that's provided in a more complex, - less readable way with `GRAMMAR EXTEND`. - -* `VERNAC COMMAND EXTEND` - adds new command syntax by adding productions to the - `command` nonterminal. For example: - - ``` - VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY - | [ "Extraction" "Library" ident(m) ] - -> { extraction_library false m } - END - ``` +very specific to Rocq (not so similar to Camlp5). - Productions here are represented with alternate syntax, described later. +Note that you can reverse engineer many details by comparing the `.mlg` input file with +the `.ml` generated by `coqpp`. - New commands should be added using this construct rather than `GRAMMAR EXTEND` so - they are correctly registered, such as having the correct command classifier. +### OCaml code - TODO: explain "ExtractionLibrary", CLASSIFIED AS, CLASSIFIED BY, "{ tactic_mode }", STATE +OCaml code enclosed in curly braces, which is copied verbatim to the generated `*.ml` file -* `VERNAC { … } EXTEND` - TODO. A variant. The `{ … }` is a block of OCaml code. +### Comments -* `TACTIC EXTEND` - adds new tactic syntax by adding productions to `simple_tactic`. - For example: +Comments in the `*.mlg` file are in the form `(* … *)`. They are not copied +to the generated `*.ml` file. Comments in OCaml code are preserved. - ``` - TACTIC EXTEND btauto - | [ "btauto" ] -> { Refl_btauto.Btauto.tac } - END - ``` +### DECLARE PLUGIN - adds a new nonterminal `btauto`. +`DECLARE PLUGIN "plugin"` - associates the file with a specific +plugin, for example "rocq-runtime.plugins.ltac". The string is the +plugin's ocamlfind name (also used to load it in the `.v` file with +`Declare ML Module`). - New tactics should be added using this construct rather than `GRAMMAR EXTEND`. +### GRAMMAR EXTEND - TODO: explain DEPRECATED, LEVEL (not shown) +`GRAMMAR EXTEND` - adds additional entries and productions to the grammar and declares global +entries referenced in the `GRAMMAR EXTEND`: -* `ARGUMENT EXTEND` - defines a new nonterminal +``` +GRAMMAR EXTEND Gram +GLOBAL: + bignat bigint …; + +END +``` - ``` - ARGUMENT EXTEND ast_closure_term - TYPED AS type_info - PRINTED BY { pp_ast_closure_term } - INTERPRETED BY { interp_ast_closure_term } - GLOBALIZED BY { glob_ast_closure_term } - SUBSTITUTED BY { subst_ast_closure_term } - RAW_PRINTED BY { pp_ast_closure_term } - GLOB_PRINTED BY { pp_ast_closure_term } - | [ term_annotation(a) constr(c) ] -> { mk_ast_closure_term a c } - END - ``` +Global entries should be available in the current OCaml scope, +eg `open Procq.Prim` makes `qualid` available. (qualified entry names are not supported) + +`GRAMMAR EXTEND` should be used only for large syntax additions. To add new commands +and tactics, use these instead: + +- `VERNAC COMMAND EXTEND` (and variant `VERNAC { entry } EXTEND`) to add new commands +- `TACTIC EXTEND` to add new ltac1 tactics +- `ARGUMENT EXTEND` to add new arguments for `TACTIC EXTEND` and `VERNAC EXTEND` +- `VERNAC ARGUMENT EXTEND` to add new arguments for `VERNAC EXTEND` - See comments in `tacentries.mli` for partial information on the various - arguments. +These constructs provide essential semantic information that's provided in a more complex, +less readable way with `GRAMMAR EXTEND`. + +### VERNAC EXTEND + +`VERNAC COMMAND EXTEND` - adds new command syntax by adding productions to the +`command` entry. + +`VERNAC { entry } EXTEND` - adds new command syntax to the `entry` entry. +This is typically used for proof modes (see also `Pvernac.register_proof_mode` and the user doc for proof modes). + +Simple example: + +``` +VERNAC COMMAND EXTEND CmdName CLASSIFIED AS SIDEFF +| [ "Cmd" arg(a) ] -> { do_interp a } +END +``` +defines a command composed of the string `Cmd` followed by argument `wit_arg`. +Running the command calls `do_interp a` where `a` is the result of parsing `arg`. + +Example with all optional elements: +``` +VERNAC COMMAND EXTEND CmdName CLASSIFIED AS SIDEFF +| #[ attr ] ![ state ] [ "Cmd" arg(a) ] + => { rule_classif a } + SYNTERP AS synv { do_synterp attr a } + -> { do_interp attr a synv } +END +``` + +Productions here are represented with [alternate syntax](#alternate-production-syntax), described later. + +Nonterminals in `VERNAC EXTEND` parsing rules (e.g. `arg` in the example) +are arguments, possibly with [nonterminal modifiers](#nonterminal-modifiers). +The name prefixed by `wit_` must be available in the current OCaml scope. -* `VERNAC ARGUMENT EXTEND` - (part of `argument_extend` in the yacc grammar) defines - productions for a single nonterminal. For example: +New commands should be added using this construct rather than `GRAMMAR EXTEND` so +they are correctly registered, such as having the correct command classifier. + +#### Extend name - ``` - VERNAC ARGUMENT EXTEND language - PRINTED BY { pr_language } - | [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml } - | [ "OCaml" ] -> { Ocaml } - | [ "Haskell" ] -> { Haskell } - | [ "Scheme" ] -> { Scheme } - | [ "JSON" ] -> { JSON } - END - ``` - - TODO: explain PRINTED BY, CODE +Each `VERNAC EXTEND` must have a unique name ("CmdName" in the example) +(unique for the plugin, you will get an anomaly at runtime if it's +not). -* DOC_GRAMMAR - Used in `doc_grammar`-generated files to permit simplified syntax +#### Classification -Note that you can reverse engineer many details by comparing the `.mlg` input file with -the `.ml` generated by `coqpp`. +Commands must be "classified" for the STM. +Classifying a command is generating a +`Vernacextend.vernac_classification` (see comments on its +declaration for the meaning of the different values). +This is done by appending one of the following annotations to the `VERNAC COMMAND EXTEND CmdName` grammar extension: +- `CLASSIFIED AS QUERY` for `VtQuery` +- `CLASSIFIED AS SIDEFF` for `VtSideff ([], VtLater)` (most commands are in this case) +- `CLASSIFIED BY { code }` where code is the classification, when it is static +- adding `{ code } =>` after the parsing rule (before its + interpretation), where `code` is the classification and has access + to argument values. + + Used when the classification is not the same for the whole block + or depends on the parsed values + (eg `| [ "foo" arg(x) ] => { classify x } -> { interpret x }`). + + Per-rule classification overrides block level classification. + Block classification should be omitted (it will be ignored) + if all rules have their own classification. + +#### State access + +Commands must explicitly declare when they use some of the global +state: the current proof state, program obligations state, and +bodies of `Qed` proofs. This is done by adding a `STATE state` +specifier for the whole block, or overriding it per-rule with `![ state ]` +before the parsing rule (after attributes if any). + +`preprocess-mlg` associates the state specifier with combinators in +`Vernactypes`, and the interpretation must have the type expected by +the combinator (except when it expects a thunk, in which case thunking is implicit). + +The following state specifiers +are understood (see `Coqpp_main.understand_state` if this isn't up to date): +- `close_proof` for `vtcloseproof`, note that closing proofs from plugin commands is buggy. +- `open_proof` for `vtopenproof`. +- `proof` for `vtmodifyproof` +- `proof_opt_query` for `vtreadproofopt` +- `proof_query` for `vtreadproof` +- `read_program` for `vtreadprogram` +- `program` for `vtmodifyprogram` +- `declare_program` for `vtdeclareprogram` +- `program_interactive` for `vtopenproofprogram` +- `opaque_access` for `vtopaqueaccess` + +So for instance `open_proof` requires the interpretation to have type `Declare.Proof.t` +(implicitly thunked), +`proof` requires it to have type `pstate:Declare.Proof.t -> Declare.Proof.t`. + +#### Attributes + +By default commands support no attributes (except for the general +attributes like `#[warnings]`). Attributes may be supported by +adding the list of supported attributes `#[ x = a; y = b ]` before +the parsing rule. `x` and `y` will be bound to the parsed attribute +in the interpretation, `a` and `b` are qualified identifiers of type +`'att Attributes.attribute`. Punning `#[ x ]` for `#[ x = x ]` is supported. +You can delay attribute interpretation (e.g. if it depends on the command arguments) +by using `Attributes.raw_attributes`. + +#### Synterp + +If the command modifies the parser or modifies state which may be +used to change the parser in a later command, these operations must +be separated from the main interpretation and done in the "synterp" +phase. The "synterp" phase does not have access to the "interp" +state (which notably includes the global env). + +This is done with `SYNTERP AS synv { synterp }`: `synterp` will be +evaluated in the synterp phase with the command arguments and attributes bound, +and its result will be bound to `synv` for the interp phase. + +### TACTIC EXTEND + +`TACTIC EXTEND` - adds new tactic (Ltac1) syntax by adding productions to `simple_tactic`. +For example: + +``` +TACTIC EXTEND field_lookup +| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> + { let (t,l) = List.sep_last lt in field_lookup f lH l t } +END +``` + +adds a new tactic `field_lookup`. + +New tactics should be added using this construct rather than `GRAMMAR EXTEND`. + +Nonterminals in `VERNAC EXTEND` parsing rules +(eg `tactic`, `constr_list`, `ne_constr_list` in the example) +are arguments, possibly with [nonterminal modifiers](#nonterminal-modifiers). +The name prefixed by `wit_` must be available in the current OCaml scope. + +TODO: explain DEPRECATED, LEVEL (not shown) + +### ARGUMENT EXTEND + +`ARGUMENT EXTEND` - defines a new argument which can be used in `TACTIC EXTEND` and `VERNAC EXTEND` + +``` +ARGUMENT EXTEND ast_closure_term + TYPED AS type_info + PRINTED BY { pp_ast_closure_term } + INTERPRETED BY { interp_ast_closure_term } + GLOBALIZED BY { glob_ast_closure_term } + SUBSTITUTED BY { subst_ast_closure_term } + RAW_PRINTED BY { pp_ast_closure_term } + GLOB_PRINTED BY { pp_ast_closure_term } + | [ term_annotation(a) constr(c) ] -> { mk_ast_closure_term a c } +END +``` + +See comments in `tacentries.mli` for partial information on the various +arguments. + +Nonterminals in `ARGUMENT EXTEND` parsing rules (eg `term_annotation` and `constr` in the example) +are entry names, possibly with [nonterminal modifiers](#nonterminal-modifiers). + +### VERNAC ARGUMENT EXTEND + +`VERNAC ARGUMENT EXTEND` - (part of `argument_extend` in the yacc grammar) defines +productions for a single nonterminal which can be used in `VERNAC EXTEND`. For example: + +``` +VERNAC ARGUMENT EXTEND ring_mod + PRINTED BY { pr_ring_mod env sigma } + | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) } + | [ "abstract" ] -> { Ring_kind Abstract } + | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) } + | [ "constants" "[" tactic(cst_tac) "]" ] -> { Const_tac(CstTac cst_tac) } + | [ "closed" "[" ne_global_list(l) "]" ] -> { Const_tac(Closed l) } + | [ "preprocess" "[" tactic(pre) "]" ] -> { Pre_tac pre } + | [ "postprocess" "[" tactic(post) "]" ] -> { Post_tac post } + | [ "setoid" constr(sth) constr(ext) ] -> { Setoid(sth,ext) } + | [ "sign" constr(sign_spec) ] -> { Sign_spec sign_spec } + | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> + { Pow_spec (Closed l, pow_spec) } + | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> + { Pow_spec (CstTac cst_tac, pow_spec) } + | [ "div" constr(div_spec) ] -> { Div_spec div_spec } +END +``` + +`PRINTED BY` specifies how the argument should be printed (used by +`-beautify`, `-time`, and various debug printers). +The `PRINTED BY` code has variables `env : Environ.env` and `sigma : Evd.evar_map` bound. + +Nonterminals in `VERNAC ARGUMENT EXTEND` (e.g. `constr`, `tactic`, `ne_global_list` in the example) +are entry names, possibly with [nonterminal modifiers](#nonterminal-modifiers). + +### DOC_GRAMMAR + +`DOC_GRAMMAR` - Used in `doc_grammar`-generated files to permit simplified syntax ## Grammars: Nonterminals and Productions @@ -242,11 +396,11 @@ productions that's similar to what's used in the `Tactic Notation` and END ``` -Nonterminals appearing in the alternate production syntax are accessed through `wit_*` symbols -defined in the OCaml code. Some commonly used symbols are defined in `stdarg.ml`. -Others are defined in the code generated by `ARGUMENT EXTEND` and `VERNAC ARGUMENT EXTEND` -constructs. References to nonterminals that don't have `wit_*` symbols cause -compilation errors. +For `VERNAC EXTEND` and `TACTIC EXTEND`, nonterminals appearing in the +alternate production syntax are "arguments" (`Genarg.genarg_type`) accessed by prefixing the name with `wit_`. Some commonly used arguments are defined in +`stdarg.ml`. Others are defined in the code generated by `ARGUMENT EXTEND` +and `VERNAC ARGUMENT EXTEND` constructs. References to +nonterminals that don't have `wit_*` symbols cause compilation errors. The differences are: * The outer `: [ … ];` is omitted. Each production is enclosed in `| [ … ]`. @@ -254,12 +408,7 @@ The differences are: * Literal strings that are valid identifiers don't become reserved keywords * No semicolons separating elements of the production * `integer(n)` is used to bind a nonterminal value to a variable instead of `n = integer` -* Alternate forms of constructs are used: - * `ne_entry_list` for `LIST1 entry` - * `entry_list` for `LIST0 entry` - * `ne_entry_list_sep(var, sep)` for `LIST1 entry SEP sep` where the list is bound to `var` - * `entry_list_sep(var, sep)` for `LIST0 entry SEP sep` where the list is bound to `var` - * `entry_opt` for OPT entry +* [nonterminal modifiers](#nonterminal-modifiers) are used * There's no way to define `LEVEL`s * There's no equivalent to `( elements )` or `[ elements1 | elements2 | … ]`, which may require repeating similar syntax several times. For example, this single production @@ -274,6 +423,21 @@ The differences are: IDENT "as"; ident -> { … } ``` +### Nonterminal modifiers + +In the alternate syntax nonterminal names may be mangled by adding +prefixes and suffixes to parse lists and options: + +* `ne_entry_list` for `LIST1 entry` +* `entry_list` for `LIST0 entry` +* `ne_entry_list_sep(var, sep)` for `LIST1 entry SEP sep` where the list is bound to `var` +* `entry_list_sep(var, sep)` for `LIST0 entry SEP sep` where the list is bound to `var` +* `entry_opt` for `OPT entry` + +This works regardless of whether the nonterminal is an entry or an +argument. The demangled entry or argument name must be available in +the current OCaml scope (with `wit_` prefix for arguments). + ## Usage notes ### Other components diff --git a/dev/doc/profiling.md b/dev/doc/profiling.md index 871400f51816..95f09b26f703 100644 --- a/dev/doc/profiling.md +++ b/dev/doc/profiling.md @@ -93,8 +93,8 @@ working on the stdlib to avoid issues with artifacts. The following command sequence will do all that: ``` opam install memtrace -dune build theories/Strings/Byte.vo # to build deps of Byte -cp theories/Strings/Byte.v ./MyByte.v -MEMTRACE=trace-byte.tcr dune exec -- dev/shim/coqc MyByte.v +make world # to build deps +cp theories/Corelib/Classes/RelationClasses.v /tmp +MEMTRACE=trace-byte.tcr dune exec -- rocq c /tmp/RelationClasses.v memtrace-viewer trace-byte.tcr ``` diff --git a/dev/shim/dune b/dev/shim/dune deleted file mode 100644 index 726529064cde..000000000000 --- a/dev/shim/dune +++ /dev/null @@ -1,128 +0,0 @@ -; -; Shims for running coq binaries with minimal dependencies -; - -; coqtop - -(alias - (name coqtop-prelude) - (deps - %{bin:coqtop} - ; XXX: bug, we are missing the dep on the _install meta file... - %{project_root}/theories/Init/Prelude.vo)) - -(rule - (targets coqtop) - (deps (alias coqtop-prelude)) - (action - (with-stdout-to %{targets} - (progn - (echo "#!/usr/bin/env bash\n") - (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'") - (run chmod +x %{targets}))))) - -; coqidetop - -(alias - (name coqidetop-prelude) - (deps - %{bin:coqidetop.opt} - ; XXX: bug, we are missing the dep on the _install meta file... - %{project_root}/theories/Init/Prelude.vo)) - -(rule - (targets coqidetop.opt) - (deps (alias coqidetop-prelude)) - (action - (with-stdout-to %{targets} - (progn - (echo "#!/usr/bin/env bash\n") - (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqidetop.opt} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'") - (run chmod +x %{targets}))))) - -; coqc - -(alias - (name coqc-prelude) - (deps - %{bin:coqc} - %{bin:rocqworker} - %{project_root}/theories/Init/Prelude.vo)) - -(rule - (targets coqc) - (deps (alias coqc-prelude)) - (action - (with-stdout-to %{targets} - (progn - (echo "#!/usr/bin/env bash\n") - (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqc} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} -nI \"$(dirname \"$0\")\"/%{project_root}/kernel/.kernel.objs/byte \"$@\"'") - (run chmod +x %{targets}))))) - -; coqtop.byte - -(alias - (name coqtop.byte-prelude) - (deps - %{project_root}/theories/Init/Prelude.vo - %{bin:coqtop.byte} - %{lib:rocq-runtime.config:config.cma} - %{lib:rocq-runtime.clib:clib.cma} - %{lib:rocq-runtime.lib:lib.cma} - %{lib:rocq-runtime.kernel:kernel.cma} - %{lib:rocq-runtime.vm:coqrun.cma} - %{lib:rocq-runtime.vm:../../stublibs/dllcoqrun_stubs.so} - %{lib:rocq-runtime.library:library.cma} - %{lib:rocq-runtime.engine:engine.cma} - %{lib:rocq-runtime.pretyping:pretyping.cma} - %{lib:rocq-runtime.gramlib:gramlib.cma} - %{lib:rocq-runtime.interp:interp.cma} - %{lib:rocq-runtime.proofs:proofs.cma} - %{lib:rocq-runtime.parsing:parsing.cma} - %{lib:rocq-runtime.printing:printing.cma} - %{lib:rocq-runtime.tactics:tactics.cma} - %{lib:rocq-runtime.vernac:vernac.cma} - %{lib:rocq-runtime.stm:stm.cma} - %{lib:rocq-runtime.sysinit:sysinit.cma} - %{lib:rocq-runtime.toplevel:toplevel.cma} - %{lib:rocq-runtime.plugins.number_string_notation:number_string_notation_plugin.cma} - %{lib:rocq-runtime.plugins.tauto:tauto_plugin.cma} - %{lib:rocq-runtime.plugins.cc:cc_plugin.cma} - %{lib:rocq-runtime.plugins.firstorder:firstorder_plugin.cma} - %{lib:rocq-runtime.plugins.ltac:ltac_plugin.cma} - (alias %{project_root}/dev/ml_toplevel_files))) - -(rule - (targets coqtop.byte) - (deps (alias coqtop.byte-prelude)) - (action - (with-stdout-to %{targets} - (progn - (echo "#!/usr/bin/env bash\n") - (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop.byte} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'") - (run chmod +x %{targets}))))) - -; rocqide - -(alias - (name rocqide-prelude) - (deps - ; without this if the gtk libs are not available dune can try to use - ; rocqide from PATH instead of giving a nice error - ; there is no problem with the other shims since they don't depend on optional build products - %{project_root}/ide/rocqide/rocqide_main.exe - %{bin:rocqworker} - %{bin:coqidetop} - %{project_root}/theories/Init/Prelude.vo - %{project_root}/coqide-server.install - %{project_root}/rocqide.install)) - -(rule - (targets rocqide) - (deps (alias rocqide-prelude)) - (action - (with-stdout-to %{targets} - (progn - (echo "#!/usr/bin/env bash\n") - (bash "echo '\"$(dirname \"$0\")\"/%{bin:rocqide} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'") - (run chmod +x %{targets}))))) diff --git a/dev/tools/list-contributors.sh b/dev/tools/list-contributors.sh index 5127ff7ae7d1..6afa02b78211 100755 --- a/dev/tools/list-contributors.sh +++ b/dev/tools/list-contributors.sh @@ -29,7 +29,7 @@ do if [[ $? == 1 ]] then echo $i" not found" - break + continue fi echo $res | tail -n1 | cut -d'<' -f1 >> reviewers-names.tmp done diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index ec1640c3f701..d04845d2a1f8 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -3,9 +3,12 @@ set -e set -o pipefail -API=https://api.github.com/repos/coq/coq -OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq" -OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" +ORG=rocq-prover +REPO=rocq + +API=https://api.github.com/repos/$ORG/$REPO +OFFICIAL_REMOTE_GIT_URL="git@github.com:$ORG/$REPO" +OFFICIAL_REMOTE_HTTPS_URL="github.com/$ORG/$REPO" # This script depends (at least) on git (>= 2.7) and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ @@ -93,7 +96,7 @@ PRDATA=$(curl -s "$API/pulls/$PR") TITLE=$(echo "$PRDATA" | jq -r '.title') info "title for PR $PR is $TITLE" -BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label') +BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.ref') info "PR $PR targets branch $BASE_BRANCH" CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) @@ -133,7 +136,7 @@ info "commit for PR $PR is $COMMIT" # Sanity check: merge to a different branch -if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then +if [ "$BASE_BRANCH" != "$CURRENT_LOCAL_BRANCH" ]; then error "PR requests merge in $BASE_BRANCH but you are merging in $CURRENT_LOCAL_BRANCH" ask_confirmation fi; @@ -147,7 +150,8 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then # Is it just that the upstream branch is behind? # It could just be that we merged other PRs and we didn't push yet - if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then + if [ "$BASE_BRANCH" = master ] \ + && git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then warning "Your branch is ahead of ${REMOTE}." warning "On master, GitHub's branch protection rule prevents merging several PRs at once." warning "You should run [git push ${REMOTE}] between each call to the merge script." diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0f3c46bf0431..a739e433050f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -664,7 +664,7 @@ let () = let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context econstr_display c) in - let cmd_class _ = VtQuery in + let cmd_class _ ~atts:_ = VtQuery in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in static_vernac_extend ~plugin:None ~command:"PrintConstr" [cmd] @@ -674,7 +674,7 @@ let () = let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context print_pure_econstr c) in - let cmd_class _ = VtQuery in + let cmd_class _ ~atts:_ = VtQuery in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in static_vernac_extend ~plugin:None ~command:"PrintPureConstr" [cmd] diff --git a/doc/changelog/01-kernel/20415-fix-fix-incon.rst b/doc/changelog/01-kernel/20415-fix-fix-incon.rst deleted file mode 100644 index 9cdacf0179cd..000000000000 --- a/doc/changelog/01-kernel/20415-fix-fix-incon.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Guard checking forgot to check non principal arguments of a fixpoint - for unguarded uses of the fixpoint leading to an inconsistency - (`#20415 `_, - fixes `#20413 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/20457-fix-guard-subterm.rst b/doc/changelog/01-kernel/20457-fix-guard-subterm.rst deleted file mode 100644 index 8517606ae6fb..000000000000 --- a/doc/changelog/01-kernel/20457-fix-guard-subterm.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - inconsistency from incomplete guard checking with nested matches - (`#20457 `_, - fixes `#20455 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/20648-fix-guard-checker-Fixed.rst b/doc/changelog/01-kernel/20648-fix-guard-checker-Fixed.rst deleted file mode 100644 index f8465476802e..000000000000 --- a/doc/changelog/01-kernel/20648-fix-guard-checker-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - inconsistency from incorrect reduction across a fixpoint during guard checking - (`#20648 `_, - fixes `#20555 `_, - by Yann Leray). diff --git a/doc/changelog/02-specification-language/20635-new-sort-sep-syntax-Added.rst b/doc/changelog/02-specification-language/20635-new-sort-sep-syntax-Added.rst deleted file mode 100644 index c4893102ecfb..000000000000 --- a/doc/changelog/02-specification-language/20635-new-sort-sep-syntax-Added.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - in :ref:`sort polymorphic ` instances, sorts can be separated from universes using `;` instead of `|`. - This is less ambiguous as `|` is also used to separate universes and constraints when declaring sort polymorphic objects, - and in such declarations when constraints are unspecified it allows omitting the `|` - (`Definition foo@{s;u} := ...` instead of `Definition foo@{s|u|+} := ...`) - (`#20635 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/20635-new-sort-sep-syntax-Deprecated.rst b/doc/changelog/02-specification-language/20635-new-sort-sep-syntax-Deprecated.rst deleted file mode 100644 index 271afcc73bd3..000000000000 --- a/doc/changelog/02-specification-language/20635-new-sort-sep-syntax-Deprecated.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - in :ref:`sort polymorphic ` instances, separating sorts from universes using `|` instead of `;` (the later being possible since this version) - (`#20635 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/20294-specif-type.rst b/doc/changelog/03-notations/20294-specif-type.rst deleted file mode 100644 index d5b3e5ee69ab..000000000000 --- a/doc/changelog/03-notations/20294-specif-type.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - The `Specif` notations (`exists x : A, P`, `{ x : A | P }`, `{ x : A & P }`, etc) - locally open `type_scope` for the second component (`P`). - This makes eg `{ x & type_1 * type_2 }` work even when `nat_scope` is opened instead of interpreting `*` as peano multiplication - (`#20294 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/20484-enable-disable-nota-fix-locality.rst b/doc/changelog/03-notations/20484-enable-disable-nota-fix-locality.rst deleted file mode 100644 index 589c3a45d087..000000000000 --- a/doc/changelog/03-notations/20484-enable-disable-nota-fix-locality.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - :cmd:`Enable Notation` and :cmd:`Disable Notation` do not take - effect in deep imports (i.e. when a parent of their origin module is - imported) - (`#20484 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/14937-abstract-no-nametab.rst b/doc/changelog/04-tactics/14937-abstract-no-nametab.rst deleted file mode 100644 index 27a010f9092c..000000000000 --- a/doc/changelog/04-tactics/14937-abstract-no-nametab.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Changed:** - the :tacn:`abstract` tactic now only registers a name - for the sublemma after the whole tactic block has run, - i.e. after a dot. In particular, the sublemma cannot - be accessed by its name while the tactic call has not - returned - (`#14937 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/19700-dependent-projectability-congruence-Changed.rst b/doc/changelog/04-tactics/19700-dependent-projectability-congruence-Changed.rst deleted file mode 100644 index 7092ad157c76..000000000000 --- a/doc/changelog/04-tactics/19700-dependent-projectability-congruence-Changed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - the congruence tactic now can handle some dependently typed constructor fields. - The field's type has to be composed of terms occuring globally or projectable from - parameters or indices of the inductive type - (`#19700 `_, - by Benedict Christian Smit). diff --git a/doc/changelog/04-tactics/19811-fix-setoid-proj-Changed.rst b/doc/changelog/04-tactics/19811-fix-setoid-proj-Changed.rst deleted file mode 100644 index 7c6f7d87c4a5..000000000000 --- a/doc/changelog/04-tactics/19811-fix-setoid-proj-Changed.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - setoid rewriting now rewrites under primitive projections. - In rare cases (see for instance - `#20575 `_), - some rewrite that used to accidentally work will now correctly fail - (`#19811 `_, - by Josselin Poiret and Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/20197-ltac2-rename.rst b/doc/changelog/04-tactics/20197-ltac2-rename.rst deleted file mode 100644 index c4e1e4eeccad..000000000000 --- a/doc/changelog/04-tactics/20197-ltac2-rename.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Add `rename`, `eassumption`, `cycle`, and `exfalso` Ltac2 notations - (`#20197 `_, - by Josselin Poiret). diff --git a/doc/changelog/04-tactics/20476-generalized-rewrite-debug-opt.rst b/doc/changelog/04-tactics/20476-generalized-rewrite-debug-opt.rst deleted file mode 100644 index 485b34116bd7..000000000000 --- a/doc/changelog/04-tactics/20476-generalized-rewrite-debug-opt.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Added a new :flag:`Rewrite Output Constraints` flag and :ref:`documented ` its use - for solving typeclass resolution failures in setoid rewriting - (`#20476 `_, - by Matthieu Sozeau). diff --git a/doc/changelog/04-tactics/20486-tc-locality.rst b/doc/changelog/04-tactics/20486-tc-locality.rst deleted file mode 100644 index e19141a27dca..000000000000 --- a/doc/changelog/04-tactics/20486-tc-locality.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - output of :cmd:`Print Instances` better matches the actual behaviour - when an instance is declared multiple times with different priorities - (`#20486 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/05-Ltac-language/20054-tac-redef-locality.rst b/doc/changelog/05-Ltac-language/20054-tac-redef-locality.rst deleted file mode 100644 index 5e5defe2c1ac..000000000000 --- a/doc/changelog/05-Ltac-language/20054-tac-redef-locality.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - :cmd:`Ltac` redefinitions (`Ltac ::=`) understand :attr:`export`. - Previously :attr:`global` and the default locality meant the redefinition would - take effect at Require time and when importing any surrounding module. - Now :attr:`global` means it takes affect at Require time, - :attr:`export` when the current module (but not its parents) is imported, - and the default is equivalent to the combination of :attr:`global` and :attr:`export` - (`#20054 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/05-Ltac-language/20391-ltac1-no-unredef.rst b/doc/changelog/05-Ltac-language/20391-ltac1-no-unredef.rst deleted file mode 100644 index 859189caddbb..000000000000 --- a/doc/changelog/05-Ltac-language/20391-ltac1-no-unredef.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - :cmd:`Ltac` redefinitions (`Ltac foo ::= ...`) are not undone by - importing the module containing the original definition. - To get the previous behaviour, add `Ltac foo ::= orig_def.` - after the original definition `Ltac foo := orig_def.` - (`#20391 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/05-Ltac-language/20511-multiple-named-goals-changed.rst b/doc/changelog/05-Ltac-language/20511-multiple-named-goals-changed.rst deleted file mode 100644 index 2b379969ecc2..000000000000 --- a/doc/changelog/05-Ltac-language/20511-multiple-named-goals-changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Named goals can now appear in any goal selector list - (`#20511 `_, - fixes `#12838 `_, - by Dario Halilovic). diff --git a/doc/changelog/06-Ltac2-language/20088-ltac2-is-sort.rst b/doc/changelog/06-Ltac2-language/20088-ltac2-is-sort.rst deleted file mode 100644 index 88788ace3ed0..000000000000 --- a/doc/changelog/06-Ltac2-language/20088-ltac2-is-sort.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - ``Ltac2.Constr.is_string``, ``Ltac2.Constr.is_sort`` - (`#20088 `_, - by Jason Gross). diff --git a/doc/changelog/06-Ltac2-language/20089-ltac2-decompose-app.rst b/doc/changelog/06-Ltac2-language/20089-ltac2-decompose-app.rst deleted file mode 100644 index 388edc249db3..000000000000 --- a/doc/changelog/06-Ltac2-language/20089-ltac2-decompose-app.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - ``Ltac2.Constr.decompose_app_list``, ``Ltac2.Constr.decompose_app`` - (`#20089 `_, - by Jason Gross). diff --git a/doc/changelog/06-Ltac2-language/20184-ltac2-option-is-some-none.rst b/doc/changelog/06-Ltac2-language/20184-ltac2-option-is-some-none.rst deleted file mode 100644 index 1acf41fbc0f9..000000000000 --- a/doc/changelog/06-Ltac2-language/20184-ltac2-option-is-some-none.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - ``Ltac2.Option.is_some``, ``Ltac2.Option.is_none``, ``Ltac2.Option.compare``, - ``Ltac2.Option.join``, ``Ltac2.Option.iter`` - (`#20184 `_, - by Jason Gross). diff --git a/doc/changelog/06-Ltac2-language/20220-better-fresh.rst b/doc/changelog/06-Ltac2-language/20220-better-fresh.rst deleted file mode 100644 index 14cdafa73abe..000000000000 --- a/doc/changelog/06-Ltac2-language/20220-better-fresh.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - `empty` and `add` in `Ltac2.Fresh.Free`, `next` in `Ltac2.Fresh`. - `Ltac2.Fresh` operations should also be faster - (`#20220 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/20313-genarg-ntn-vars.rst b/doc/changelog/06-Ltac2-language/20313-genarg-ntn-vars.rst deleted file mode 100644 index b51714152102..000000000000 --- a/doc/changelog/06-Ltac2-language/20313-genarg-ntn-vars.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Fixed:** - Ltac2 in terms in notations is more aware of the notation variables it uses, - providing early failure when the variable is instantiated with an invalid term, - preventing a spurious warning when a variable that cannot be instantiated is unused, - and preventing exponential blowups from copying unused data - (`#20313 `_, - fixes `#17833 `_ - and `#20188 `_ - and `#20305 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/20387-ltac2-noinit.rst b/doc/changelog/06-Ltac2-language/20387-ltac2-noinit.rst deleted file mode 100644 index 8639a10e8586..000000000000 --- a/doc/changelog/06-Ltac2-language/20387-ltac2-noinit.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Ltac2 does not depend on the prelude (i.e. it is compiled with `-noinit`). - It still depends on `Corelib.Init.Ltac` due to the interoperation with Ltac1 - (`#20387 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/20430-lconstr_in_ltac.rst b/doc/changelog/06-Ltac2-language/20430-lconstr_in_ltac.rst deleted file mode 100644 index 2e765412b08e..000000000000 --- a/doc/changelog/06-Ltac2-language/20430-lconstr_in_ltac.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Enable use of (open\_)lconstr inside Ltac2 Notation command - (`#20430 `_, - by Pim Otte). diff --git a/doc/changelog/06-Ltac2-language/20475-ltac2_expose_inductive.rst b/doc/changelog/06-Ltac2-language/20475-ltac2_expose_inductive.rst deleted file mode 100644 index 9f3bf8cc066b..000000000000 --- a/doc/changelog/06-Ltac2-language/20475-ltac2_expose_inductive.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - API functions for inductive types - `Ind.nparams`, `Ind.nparams_uniform`, `Ind.constructor_nargs`, `Ind.constructor_ndecls`, `Constr.Case.inductive` - (`#20475 `_, - fixes `#10940 `_, - by Patrick Nicodemus). diff --git a/doc/changelog/06-Ltac2-language/20498-ltac2-format-alpha.rst b/doc/changelog/06-Ltac2-language/20498-ltac2-format-alpha.rst deleted file mode 100644 index c228e04076b3..000000000000 --- a/doc/changelog/06-Ltac2-language/20498-ltac2-format-alpha.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - format specifiers `%A` to use unthunked printers and `%m` for already-formatted messages. - Typically, instead of `printf "foo: %a" (fun () v => print_thing v) v` - we can now write `printf "foo: %A" print_thing v` - or `printf "foo: %m" (print_thing v)` - (`#20498 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/20504-ltac2-scope-entry-Changed.rst b/doc/changelog/06-Ltac2-language/20504-ltac2-scope-entry-Changed.rst deleted file mode 100644 index 6f69105d2aac..000000000000 --- a/doc/changelog/06-Ltac2-language/20504-ltac2-scope-entry-Changed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - the documentation and error messages do not use the term "scope" to describe Ltac2 :ref:`syntactic_classes` - (`#20504 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/20516-ltac2-set-export-Changed.rst b/doc/changelog/06-Ltac2-language/20516-ltac2-set-export-Changed.rst deleted file mode 100644 index 32e26c11bd98..000000000000 --- a/doc/changelog/06-Ltac2-language/20516-ltac2-set-export-Changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - :cmd:`Ltac2 Set` only takes effect with shallow imports, i.e. - `Import Foo` will not run a mutation from (non exported) inner module `Foo.Bar` - (`#20516 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/20543-radrow-gh-20482-reductions-Added.rst b/doc/changelog/06-Ltac2-language/20543-radrow-gh-20482-reductions-Added.rst deleted file mode 100644 index 8ddc29dc0bdc..000000000000 --- a/doc/changelog/06-Ltac2-language/20543-radrow-gh-20482-reductions-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Ltac2 type for reduction expressions - (`#20543 `_, - by Radosław Rowicki, with review of Pierre-Marie Pédrot and Gaëtan Gilbert and Jason Gross). diff --git a/doc/changelog/06-Ltac2-language/20544-radrow-gh-20482-rewrite_strat-Added.rst b/doc/changelog/06-Ltac2-language/20544-radrow-gh-20482-rewrite_strat-Added.rst deleted file mode 100644 index 5ca592576170..000000000000 --- a/doc/changelog/06-Ltac2-language/20544-radrow-gh-20482-rewrite_strat-Added.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Ported `rewrite_strat` to Ltac2 and added the `Rewrite.Strategy` module for describing rewrite strategies - (`#20544 `_, - fixes `#20482 `_, - by Radosław Rowicki with review of Jason Gross and Pierre-Marie Pédrot and Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/20547-ltac2-message-empty.rst b/doc/changelog/06-Ltac2-language/20547-ltac2-message-empty.rst deleted file mode 100644 index 11127e51b67a..000000000000 --- a/doc/changelog/06-Ltac2-language/20547-ltac2-message-empty.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - ``Ltac2.Message.empty`` - (`#20547 `_, - by Elyes Jemel). diff --git a/doc/changelog/06-Ltac2-language/20549-ltac2-add-Ltac1CompatNotations.md b/doc/changelog/06-Ltac2-language/20549-ltac2-add-Ltac1CompatNotations.md deleted file mode 100644 index 75f0894913ca..000000000000 --- a/doc/changelog/06-Ltac2-language/20549-ltac2-add-Ltac1CompatNotations.md +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - A file Ltac1CompatNotations.v for Ltac2 Notations reproducing Ltac1 parsing of tactics, - that can be harmful to parsing, and produce bad error messages. - (`#20569 `_, - by Thomas Lamiaux). diff --git a/doc/changelog/06-Ltac2-language/20649-ltac2-add-conv-to-unification.rst b/doc/changelog/06-Ltac2-language/20649-ltac2-add-conv-to-unification.rst deleted file mode 100644 index 58667878acc1..000000000000 --- a/doc/changelog/06-Ltac2-language/20649-ltac2-add-conv-to-unification.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Add conversion tests to Unification - `Unification.conv`, `Unification.conv_current`, `Unification.conv_full` - (`#20649 `_, - fixes `#20579 `_, - by Thomas Lamiaux). diff --git a/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_added.rst b/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_added.rst deleted file mode 100644 index caf7094f0cf2..000000000000 --- a/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_added.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - definitions `injective2`, `idempotent_op` and `idempotent_fun` and - lemmas `omap_id`, `eq_omap`, `inj_omap`, `omapK`, `inr_inj` and - `inl_inj` in `ssrfun.v` - (`#20478 `_, - by Pierre Roux). diff --git a/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_changed.rst b/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_changed.rst deleted file mode 100644 index 22e11dcf5a01..000000000000 --- a/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - `%FUN` now delimits scope `function_scope` rather than `fun_scope` - in `ssrfun.v` - (`#20478 `_, - by Pierre Roux). diff --git a/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_deprecated.rst b/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_deprecated.rst deleted file mode 100644 index ef7793a849bd..000000000000 --- a/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_deprecated.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - `idempotent` in `ssrfun.v`, use `idempotent_op` instead - (`#20478 `_, - by Pierre Roux). diff --git a/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_removed.rst b/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_removed.rst deleted file mode 100644 index 4b9249efcd0e..000000000000 --- a/doc/changelog/07-ssreflect/20478-mathcomp_backport_20250407_removed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - scope `fun_scope` from `ssrfun.v` that was deprecated since 8.20, - use `function_scope` instead - (`#20478 `_, - by Pierre Roux). diff --git a/doc/changelog/08-vernac-commands-and-options/18615-decl-sort.rst b/doc/changelog/08-vernac-commands-and-options/18615-decl-sort.rst deleted file mode 100644 index bd3149152e78..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/18615-decl-sort.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - :cmd:`Sort` to declare global or section-scoped sort qualities - (`#18615 `_, - by Kenji Maillard). diff --git a/doc/changelog/08-vernac-commands-and-options/19690-ltacX-obligations.rst b/doc/changelog/08-vernac-commands-and-options/19690-ltacX-obligations.rst deleted file mode 100644 index c0a0e7b8178c..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/19690-ltacX-obligations.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - commands taking a tactic argument (e.g. :cmd:`Hint Extern`) - now follow :opt:`Default Proof Mode` instead of hardcoding Ltac1 - (`#19690 `_, - fixes `#13784 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/20107-number-nota.rst b/doc/changelog/08-vernac-commands-and-options/20107-number-nota.rst deleted file mode 100644 index c034642fbea5..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/20107-number-nota.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - :cmd:`Number Notation` and :cmd:`String Notation` understand parsers which may produce error messages - (`#20107 `_, - fixes `#20042 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/20275-constrextern-max-depth.rst b/doc/changelog/08-vernac-commands-and-options/20275-constrextern-max-depth.rst deleted file mode 100644 index c984d7035818..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/20275-constrextern-max-depth.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - :opt:`Printing Depth` completely skips subterms beyond the given depth. - In general the formatter depth is higher than the term depth, so there is no visible change, - but some notations print subterms without increasing the formatting depth in which case - you may need to increase the printing depth to avoid `...` - (`#20275 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/20349-search-filter-local.rst b/doc/changelog/08-vernac-commands-and-options/20349-search-filter-local.rst deleted file mode 100644 index 2e2ed566b1ee..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/20349-search-filter-local.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - :cmd:`Search` ignores lemmas declared with :attr:`local` unless - new flag :flag:`Search Blacklist Locals` is unset - (`#20349 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/20355-refine-definition.rst b/doc/changelog/08-vernac-commands-and-options/20355-refine-definition.rst deleted file mode 100644 index 7c6150d235a5..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/20355-refine-definition.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Added the #[refine] attribute to definitions and (co)fixpoints - (`#20355 `_, - fixes `#20302 `_, - by Yann Leray). diff --git a/doc/changelog/08-vernac-commands-and-options/20640-lia-noenum-Removed.rst b/doc/changelog/08-vernac-commands-and-options/20640-lia-noenum-Removed.rst deleted file mode 100644 index 66d9d7532e5b..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/20640-lia-noenum-Removed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - flag `Lia Enum`, which did nothing - (`#20640 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/20733-search-in-open-module.rst b/doc/changelog/08-vernac-commands-and-options/20733-search-in-open-module.rst deleted file mode 100644 index 4438789711d9..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/20733-search-in-open-module.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - :cmd:`Search` now accepts open modules, including the current file with - the `in`, `inside` and `outside` filters. - (`#20733 `_, - fixes `#14010 `_, - by Pierre Rousselin, with a lot of help by Gaëtan Gilbert). diff --git a/doc/changelog/09-cli-tools/20169-devtools.rst b/doc/changelog/09-cli-tools/20169-devtools.rst deleted file mode 100644 index d60c4e0c2d1c..000000000000 --- a/doc/changelog/09-cli-tools/20169-devtools.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - `rocq timelog2html` now needs package `rocq-devtools` to be installed - (`#20169 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/09-cli-tools/20393-coqdep-implicit-i.rst b/doc/changelog/09-cli-tools/20393-coqdep-implicit-i.rst deleted file mode 100644 index 69918cd64439..000000000000 --- a/doc/changelog/09-cli-tools/20393-coqdep-implicit-i.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Fixed:** - `rocq dep` implicitly adds `-I $rocq-runtime/..` after the explicit `-I` instead of before - (where `$rocq-runtime` is the expected location of the rocq-runtime package). - This means that if a local plugin (whose META is in an explicit `-I` path) is installed next to rocq-runtime, - `rocq dep` will emit a dependency on the local version instead of the installed version - (`#20393 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/09-cli-tools/20601-find-unique-Changed.rst b/doc/changelog/09-cli-tools/20601-find-unique-Changed.rst deleted file mode 100644 index 9280d66ab2d1..000000000000 --- a/doc/changelog/09-cli-tools/20601-find-unique-Changed.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - error on ambiguous :cmd:`Require`. Rocq used to silently select a file - when ambiguous :cmd:`Require`\s came from different loadpaths, for instance - different fields of the ``ROCQPATH`` environment variable - (`#20601 `_, - fixes `#20587 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/10-rocqide/20256-ide-charset.rst b/doc/changelog/10-rocqide/20256-ide-charset.rst deleted file mode 100644 index 01e6b6a087ba..000000000000 --- a/doc/changelog/10-rocqide/20256-ide-charset.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - default character encoding is UTF8 (it was locale dependent on non-windows OSes), - and when the configured encoding is not UTF8 RocqIDE will attempt to convert input files even if they are already valid UTF8 - (`#20256 `_, - fixes `#11526 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/10-rocqide/20597-rocqide-buffer-length-option-Fixed.rst b/doc/changelog/10-rocqide/20597-rocqide-buffer-length-option-Fixed.rst deleted file mode 100644 index 1f3160dea596..000000000000 --- a/doc/changelog/10-rocqide/20597-rocqide-buffer-length-option-Fixed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - added an option to control the maximum length of the message view - in RocqIDE - (`#20597 `_, - fixes `#20420 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/11-standard-library/20107-number-nota.rst b/doc/changelog/11-standard-library/20107-number-nota.rst deleted file mode 100644 index 929d5059a81e..000000000000 --- a/doc/changelog/11-standard-library/20107-number-nota.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - type `result` in `Corelib.Datatypes`, equivalent to `sum` - but with a name fitting possibly-failing computations - (`#20107 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/12-infrastructure-and-dependencies/19901-changelog-reloc.rst b/doc/changelog/12-infrastructure-and-dependencies/19901-changelog-reloc.rst deleted file mode 100644 index f42858b2e1f6..000000000000 --- a/doc/changelog/12-infrastructure-and-dependencies/19901-changelog-reloc.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Rocq can be compile-time configured to be relocatable, - using `./configure -relocatable` instead of e.g. `./configure -prefix /some/path`. - See :ref:`system_config` for an explanation of how Rocq uses its configured installation paths - (`#19901 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/12-infrastructure-and-dependencies/20437-fix_20422.rst b/doc/changelog/12-infrastructure-and-dependencies/20437-fix_20422.rst deleted file mode 100644 index f1fac3b5b744..000000000000 --- a/doc/changelog/12-infrastructure-and-dependencies/20437-fix_20422.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Bad interaction between dune, `rocq dep`, and local opam directory switches - (`#20437 `_, - fixes `#20422 `_, - by Rodolphe Lepigre). diff --git a/doc/changelog/12-infrastructure-and-dependencies/20464-ci+win_native.rst b/doc/changelog/12-infrastructure-and-dependencies/20464-ci+win_native.rst deleted file mode 100644 index fd690631aa73..000000000000 --- a/doc/changelog/12-infrastructure-and-dependencies/20464-ci+win_native.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Added:** Experimental support for native Windows builds. - Rocq can now build and run under a native Windows environment using - the new native Windows support in Opam 2.3. This setup is tested in - CI, running a large part of the test suite. Beware this support is - still experimental, and some problem may arise on Unix-specific - tools. Note that RocqIDE is still not supported (c.f. `#20631 - `_) (`#20464 - `_, by Emilio Jesus - Gallego Arias, Gaëtan Gilbert, David Allsopp, Ali Caglayan, Jason - Gross, the Opam team, the @setup-ocaml team, the OCaml team). diff --git a/doc/changelog/12-infrastructure-and-dependencies/20576-old-ocaml-Changed.rst b/doc/changelog/12-infrastructure-and-dependencies/20576-old-ocaml-Changed.rst deleted file mode 100644 index f8e096091506..000000000000 --- a/doc/changelog/12-infrastructure-and-dependencies/20576-old-ocaml-Changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - minimum supported OCaml version is now 4.14.0 (instead of 4.09.0), - and minimum supported OCamlfind version is now 1.9.1 (instead of 1.8.1) - (`#20576 `_, - by Gaëtan Gilbert). diff --git a/doc/dune b/doc/dune.disabled similarity index 59% rename from doc/dune rename to doc/dune.disabled index ad074acda910..1ac6f902c5d7 100644 --- a/doc/dune +++ b/doc/dune.disabled @@ -14,8 +14,10 @@ ; + config/coq_config.py ; + tools/coqdoc/coqdoc.css (package rocq-runtime) + (package rocq-core) (source_tree sphinx) (source_tree tools/coqrst) + ../config/coq_config.py unreleased.rst (env_var SPHINXWARNOPT) (env_var COQRST_EXTRA))) @@ -24,17 +26,7 @@ (targets (dir refman-html)) (alias refman-html) - ; Cannot use this deps alias because of ocaml/dune#3415 - ; (deps (alias refman-deps)) - ; EJGA: note this should've been fixed in dune master as of 05/03/2021 - (deps - (package rocq-runtime) - (source_tree sphinx) - (source_tree tools/coqrst) - ../config/coq_config.py - unreleased.rst - (env_var SPHINXWARNOPT) - (env_var COQRST_EXTRA)) + (deps (alias refman-deps)) (action (run env sphinx-build -q %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets}))) @@ -42,18 +34,7 @@ (targets (dir refman-pdf)) (alias refman-pdf) - ; Cannot use this deps alias because of ocaml/dune#3415 - ; (deps (alias refman-deps)) - ; EJGA: note this should've been fixed in dune master as of 05/03/2021 - (deps - (package rocq-runtime) - (source_tree sphinx) - (source_tree tools/coqrst) - ../config/coq_config.py - ../ide/rocqide/coq.png - unreleased.rst - (env_var SPHINXWARNOPT) - (env_var COQRST_EXTRA)) + (deps ../ide/rocqide/coq.png (alias refman-deps)) (action (progn (run env sphinx-build -q %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets}) diff --git a/doc/plugin_tutorial/.gitignore b/doc/plugin_tutorial/.gitignore index 3e4978fac48d..251ea1874a2a 100644 --- a/doc/plugin_tutorial/.gitignore +++ b/doc/plugin_tutorial/.gitignore @@ -1,6 +1,8 @@ *.ml*.d *.cm[ixt]* -Makefile.coq* +Makefile.rocq* +!Makefile.*.local +tuto0/src/META* *~ *.[ao] .coqdeps.d diff --git a/doc/plugin_tutorial/Makefile b/doc/plugin_tutorial/Makefile index 7f1833fadd45..be119b957bed 100644 --- a/doc/plugin_tutorial/Makefile +++ b/doc/plugin_tutorial/Makefile @@ -3,7 +3,8 @@ TUTOS:= \ tuto0 \ tuto1 \ tuto2 \ - tuto3 + tuto3 \ + tuto4 all: $(TUTOS) diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md index 15e83b0ea06b..1a7438ee4c7a 100644 --- a/doc/plugin_tutorial/README.md +++ b/doc/plugin_tutorial/README.md @@ -1,32 +1,32 @@ -How to write plugins in Coq +How to write plugins in Rocq =========================== - This document describes how to extend Coq by writing plugins in the - [OCaml](https://ocaml.org/) functional programming language. - Before writing a plugin, you should consider whether easier approaches - can achieve your goal. It is often easier to use an - extension language such as Ltac2 or Elpi. Ltac2 is documented in the - [refman](https://rocq-prover.org/refman/proof-engine/ltac2.html) - and Elpi comes with excellent - [tutorials](https://github.com/LPCIC/coq-elpi/#tutorials). Plugin - development is harder due to the lower level OCaml API it uses. - It is also more maintenance intensive because the OCaml API can - change from release to release without any backward compatibility - (it's not uncommon for plugins to only work with a given - version of Coq). - - # Working environment - - In addition to installing OCaml and Coq, you need to make sure that you also have the development - headers for Coq, because you will need them to compile extensions. If you installed Coq from source or - from [OPAM](http://opam.ocaml.org/doc/Install.html), you already have the required headers. If you - installed them from your system package manager, there may be a separate package - which contains the development headers (for example, in Ubuntu they are contained in the package - `libcoq-ocaml-dev`). It can help to install several tools for development. - - ## Tuareg and Merlin - - These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) +This document describes how to extend Rocq by writing plugins in the +[OCaml](https://ocaml.org/) functional programming language. +Before writing a plugin, you should consider whether easier approaches +can achieve your goal. It is often easier to use an +extension language such as Ltac2 or Elpi. Ltac2 is documented in the +[refman](https://rocq-prover.org/refman/proof-engine/ltac2.html) +and Elpi comes with excellent +[tutorials](https://github.com/LPCIC/coq-elpi/#tutorials). Plugin +development is harder due to the lower level OCaml API it uses. +It is also more maintenance intensive because the OCaml API can +change from release to release without any backward compatibility +(it's not uncommon for plugins to only work with a given +version of Rocq). + +# Working environment + +In addition to installing OCaml and Rocq, you need to make sure that you also have the development +headers for Rocq, because you will need them to compile extensions. If you installed Rocq from source or +from [OPAM](http://opam.ocaml.org/doc/Install.html), you already have the required headers. If you +installed them from your system package manager, there may be a separate package +which contains the development headers (for example, in Ubuntu they are contained in the package +`libcoq-ocaml-dev`). It can help to install several tools for development. + +## Tuareg and Merlin + +These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) ```shell opam install merlin # prints instructions for vim and emacs @@ -34,18 +34,18 @@ opam install tuareg # syntax highlighting for OCaml opam user-setup install # automatically configures editors for merlin ``` - Adding this line to your .emacs helps Tuareg recognize the .mlg extension: +Adding this line to your .emacs helps Tuareg recognize the .mlg extension: ```shell (add-to-list 'auto-mode-alist '("\\.mlg$" . tuareg-mode) t) ``` - If you are using [vscoq](https://github.com/coq-community/vscoq), - you will need to ensure that vscoq loads the `_CoqProject` file for the extension - you are working on. You can do this by opening Visual Studio Code with the `_CoqProject` - file in the project root directory, or by editing the `coqtop.coqProjectRoot` setting for vscoq. +If you are using [vscoq](https://github.com/coq-community/vscoq), +you will need to ensure that vscoq loads the `_CoqProject` file for the extension +you are working on. You can do this by opening Visual Studio Code with the `_CoqProject` +file in the project root directory, or by editing the `coqtop.coqProjectRoot` setting for vscoq. - ## This tutorial +## This tutorial ```shell cd plugin_tutorials/tuto0 @@ -53,57 +53,71 @@ make .merlin # run before opening .ml files in your editor make # build ``` - # tuto0 : basics of project organization - package an mlg file in a plugin, organize a `Makefile`, `_CoqProject` - - Example of syntax to add a new toplevel command - - Example of function call to print a simple message - - Example of function call to print a simple warning - - Example of function call to raise a simple error to the user - - Example of syntax to add a simple tactic - (that does nothing and prints a message) - - To use it: +# tuto0 : basics of project organization +package an mlg file in a plugin, organize a `Makefile`, `_CoqProject` (note comments in those files) +- Example of syntax to add a new toplevel command +- Example of function call to print a simple message +- Example of function call to print a simple warning +- Example of function call to raise a simple error to the user +- Example of syntax to add a simple tactic + (that does nothing and prints a message) +- To use it: ```bash - cd tuto0; make - coqtop -I src -R theories Tuto0 + cd tuto0; make + rocq top -I src -R theories Tuto0 ``` - In the Coq session type: +In the Rocq session type: ```coq - Require Import Tuto0.Loader. HelloWorld. + Require Import Tuto0.Loader. HelloWorld. ``` - You can also modify and run `theories/Demo.v`. - - # tuto1 : OCaml to Coq communication - Explore the memory of Coq, modify it - - Commands that take arguments: strings, integers, symbols, expressions of the calculus of constructions - - Examples of using environments correctly - - Examples of using state (the evar_map) correctly - - Commands that interact with type-checking in Coq - - A command that checks convertibility between two terms - - A command that adds a new definition or theorem - - A command that uses a name and exploits the existing definitions or theorems - - A command that exploits an existing ongoing proof - - A command that defines a new tactic - - Compilation and loading must be performed as for `tuto0`. - - # tuto2 : OCaml to Coq communication - A more step by step introduction to writing commands - - Explanation of the syntax of entries - - Adding a new type to and parsing to the available choices - - Handling commands that store information in user-chosen registers and tables - - Compilation and loading must be performed as for `tuto0`. - - # tuto3 : manipulating terms of the calculus of constructions - Manipulating terms, inside commands and tactics. - - Obtaining existing values from memory - - Composing values - - Verifying types - - Using these terms in commands - - Using these terms in tactics - - Automatic proofs without tactics using type classes and canonical structures - - compilation and loading must be performed as for `tuto0`. +You can also modify and run `theories/Demo.v`. + +Because the `.mlpack` file format does not support comments, we +explain it here: this file is used by `rocq makefile` to compile the +plugin. It lists the OCaml modules used in the plugin in dependency +order. From `foo.mlpack`, `rocq makefile` will build `foo.cma` +(bytecode plugin) and `foo.cmxs` (native plugin), so the file names in +the `META` file must match this. + +# tuto1 : OCaml to Rocq communication +Explore the memory of Rocq, modify it +- Commands that take arguments: strings, integers, symbols, expressions of the calculus of constructions +- Examples of using environments correctly +- Examples of using state (the evar_map) correctly +- Commands that interact with type-checking in Rocq +- A command that checks convertibility between two terms +- A command that adds a new definition or theorem +- A command that uses a name and exploits the existing definitions or theorems +- A command that exploits an existing ongoing proof +- A command that defines a new tactic + +Compilation and loading must be performed as for `tuto0`. + +# tuto2 : OCaml to Rocq communication +A more step by step introduction to writing commands +- Explanation of the syntax of entries +- Adding a new type to and parsing to the available choices +- Handling commands that store information in user-chosen registers and tables + +Compilation and loading must be performed as for `tuto0`. + +# tuto3 : manipulating terms of the calculus of constructions +Manipulating terms, inside commands and tactics. +- Obtaining existing values from memory +- Composing values +- Verifying types +- Using these terms in commands +- Using these terms in tactics +- Automatic proofs without tactics using type classes and canonical structures + +Compilation and loading must be performed as for `tuto0`. + +# tuto4: extending Ltac2 +Define new primitives ("externals") for Ltac2. + +Note that in this case we have no `.mlg` file, but the `Loader.v` is less trivial. + +Compilation and loading must be performed as for `tuto0`. diff --git a/doc/plugin_tutorial/tuto0/.gitignore b/doc/plugin_tutorial/tuto0/.gitignore new file mode 100644 index 000000000000..19837ad55016 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/.gitignore @@ -0,0 +1 @@ +/src/META.rocq-plugin-tutorial diff --git a/doc/plugin_tutorial/tuto0/Makefile b/doc/plugin_tutorial/tuto0/Makefile index b042cc842fa0..72f33e778a82 100644 --- a/doc/plugin_tutorial/tuto0/Makefile +++ b/doc/plugin_tutorial/tuto0/Makefile @@ -1,14 +1,15 @@ -ifeq "$(COQBIN)" "" - COQBIN=$(dir $(shell which rocq))/ -endif +# define COQBIN to the empty string if it's not already defined +# (in case we want to run make with --warn-undefined-variables) +COQBIN?= +# all unknown targets depend on the generated Rocq makefile %: Makefile.rocq +# rule to generate the Rocq makefile Makefile.rocq: _CoqProject $(COQBIN)rocq makefile -f _CoqProject -o Makefile.rocq -tests: all - @$(MAKE) -C tests -s clean - @$(MAKE) -C tests -s all - +# use the generated Rocq makefile +# -include instead of include: don't error if it's not there +# (IIRC some version of make doesn't realize that it should be built if we don't use -include) -include Makefile.rocq diff --git a/doc/plugin_tutorial/tuto0/_CoqProject b/doc/plugin_tutorial/tuto0/_CoqProject index 013a63502023..243ca6b729ac 100644 --- a/doc/plugin_tutorial/tuto0/_CoqProject +++ b/doc/plugin_tutorial/tuto0/_CoqProject @@ -1,11 +1,28 @@ -src/META.rocq-plugin-tutorial +# Comments in _CoqProject start with # and end with newline + +# .v files in theories/ are modules whose name starts with "Tuto0" -R theories/ Tuto0 + +# META (an ocamlfind library specification) is necessary for rocq to find the plugin +# in tuto0 we use rocq makefile's "-generate-meta-for-package" +# it assumes that the plugin is called rocq-plugin-tutorial.plugin +# and depends on ltac1 (rocq-runtime.plugins.ltac) +# see tuto1 for an example of a custom META file +-generate-meta-for-package rocq-plugin-tutorial + +# rocq makefile uses -I to tell the ocaml compiler where previously compiled files are located +# (in our case g_tuto0 depends on tuto0_main) -I src +# list our .v files theories/Loader.v theories/Demo.v +# list our ocaml files src/tuto0_main.ml src/tuto0_main.mli src/g_tuto0.mlg + +# mlpack is a "rocq makefile" specific file +# cf plugin tutorial README src/tuto0_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto0/src/META.rocq-plugin-tutorial b/doc/plugin_tutorial/tuto0/src/META.rocq-plugin-tutorial deleted file mode 100644 index 2aafedcc0e6d..000000000000 --- a/doc/plugin_tutorial/tuto0/src/META.rocq-plugin-tutorial +++ /dev/null @@ -1,11 +0,0 @@ -package "tuto0" ( - directory = "." - version = "dev" - description = "A tuto0 plugin" - requires = "rocq-runtime.plugins.ltac" - archive(byte) = "tuto0_plugin.cma" - archive(native) = "tuto0_plugin.cmxa" - plugin(byte) = "tuto0_plugin.cma" - plugin(native) = "tuto0_plugin.cmxs" -) -directory = "." diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg index 78ad467c3464..8a1fc6f8c997 100644 --- a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg +++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg @@ -1,4 +1,6 @@ -DECLARE PLUGIN "rocq-plugin-tutorial.tuto0" +(** See dev/doc/parsing.md for mlg doc *) + +DECLARE PLUGIN "rocq-plugin-tutorial.plugin" { @@ -8,7 +10,7 @@ open Ltac_plugin let cat = CWarnings.create_category ~name:"plugin-tuto-cat" () let tuto_warn = CWarnings.create ~name:"name" ~category:cat - (fun _ -> strbrk Tuto0_main.message) + (fun () -> strbrk Tuto0_main.message) } @@ -27,7 +29,7 @@ END *) TACTIC EXTEND hello_world_tactic | [ "hello_world" ] -> - { let _ = Feedback.msg_notice (str Tuto0_main.message) in + { let () = Feedback.msg_notice (str Tuto0_main.message) in Tacticals.tclIDTAC } END @@ -51,7 +53,7 @@ END TACTIC EXTEND hello_warning_tactic | [ "hello_warning" ] -> { - let _ = tuto_warn () in + let () = tuto_warn () in Tacticals.tclIDTAC } END @@ -71,6 +73,5 @@ END *) TACTIC EXTEND hello_error_tactic | [ "hello_error" ] -> - { let _ = CErrors.user_err (str Tuto0_main.message) in - Tacticals.tclIDTAC } + { CErrors.user_err (str Tuto0_main.message) } END diff --git a/doc/plugin_tutorial/tuto0/theories/Loader.v b/doc/plugin_tutorial/tuto0/theories/Loader.v index 13254500e238..5bea183bb627 100644 --- a/doc/plugin_tutorial/tuto0/theories/Loader.v +++ b/doc/plugin_tutorial/tuto0/theories/Loader.v @@ -1 +1 @@ -Declare ML Module "rocq-plugin-tutorial.tuto0". +Declare ML Module "rocq-plugin-tutorial.plugin". diff --git a/doc/plugin_tutorial/tuto1/META.rocq-plugin-tutorial b/doc/plugin_tutorial/tuto1/META.rocq-plugin-tutorial new file mode 100644 index 000000000000..2f720179c7f9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/META.rocq-plugin-tutorial @@ -0,0 +1,29 @@ +# Comments in META start with # and end with newline + +# our plugin is called rocq-plugin-tutorial.tuto1 +# rocq-plugin-tutorial from the META filename +# tuto1 from this "package" name +package "tuto1" ( + # the plugin files are in "src" + directory = "src" + + version = "dev" + description = "A tuto1 plugin" + + # we define ltac1 tactics so we depend on ltac + # otherwise we would depend only on rocq-runtime.vernac + # (it contains the APIs for declaring new commands) + # (ltac depends on vernac so if we depend on ltac, vernac is also implicitly depended on) + requires = "rocq-runtime.plugins.ltac" + + # the compiled plugin files (rocq makefile bases these filenames on the .mlpack filename) + # (only the "plugin" keys are used by rocq, + # "archive" is for packages which depend on this package) + archive(byte) = "tuto1_plugin.cma" + archive(native) = "tuto1_plugin.cmxa" + plugin(byte) = "tuto1_plugin.cma" + plugin(native) = "tuto1_plugin.cmxs" +) + +# paths in this file are relative to this directory +directory = "." diff --git a/doc/plugin_tutorial/tuto1/Makefile b/doc/plugin_tutorial/tuto1/Makefile index b042cc842fa0..8fdad97450fd 100644 --- a/doc/plugin_tutorial/tuto1/Makefile +++ b/doc/plugin_tutorial/tuto1/Makefile @@ -1,14 +1,8 @@ -ifeq "$(COQBIN)" "" - COQBIN=$(dir $(shell which rocq))/ -endif +COQBIN?= %: Makefile.rocq Makefile.rocq: _CoqProject $(COQBIN)rocq makefile -f _CoqProject -o Makefile.rocq -tests: all - @$(MAKE) -C tests -s clean - @$(MAKE) -C tests -s all - -include Makefile.rocq diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject index 29b670954b36..5ba83cc232f3 100644 --- a/doc/plugin_tutorial/tuto1/_CoqProject +++ b/doc/plugin_tutorial/tuto1/_CoqProject @@ -1,6 +1,14 @@ -src/META.rocq-plugin-tutorial +META.rocq-plugin-tutorial -R theories Tuto1 + +# rocq makefile uses -I in 2 ways: +# to tell rocq where the META file is located +-I . +# and to tell the ocaml compiler where previously compiled files are located +# (eg g_tuto1 depends on inspector) -I src +# in tuto0 with -generate-meta-for-package, the META was generated next to the mlpack +# so -I src did both jobs theories/Loader.v theories/Demo.v diff --git a/doc/plugin_tutorial/tuto1/src/META.rocq-plugin-tutorial b/doc/plugin_tutorial/tuto1/src/META.rocq-plugin-tutorial deleted file mode 100644 index f35e03d21f22..000000000000 --- a/doc/plugin_tutorial/tuto1/src/META.rocq-plugin-tutorial +++ /dev/null @@ -1,11 +0,0 @@ -package "tuto1" ( - directory = "." - version = "dev" - description = "A tuto1 plugin" - requires = "rocq-runtime.plugins.ltac" - archive(byte) = "tuto1_plugin.cma" - archive(native) = "tuto1_plugin.cmxa" - plugin(byte) = "tuto1_plugin.cma" - plugin(native) = "tuto1_plugin.cmxs" -) -directory = "." diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 18abfd5ffe2a..18c79728a53c 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -1,3 +1,5 @@ +(** See dev/doc/parsing.md for mlg doc *) + DECLARE PLUGIN "rocq-plugin-tutorial.tuto1" { diff --git a/doc/plugin_tutorial/tuto2/Makefile b/doc/plugin_tutorial/tuto2/Makefile index b042cc842fa0..8fdad97450fd 100644 --- a/doc/plugin_tutorial/tuto2/Makefile +++ b/doc/plugin_tutorial/tuto2/Makefile @@ -1,14 +1,8 @@ -ifeq "$(COQBIN)" "" - COQBIN=$(dir $(shell which rocq))/ -endif +COQBIN?= %: Makefile.rocq Makefile.rocq: _CoqProject $(COQBIN)rocq makefile -f _CoqProject -o Makefile.rocq -tests: all - @$(MAKE) -C tests -s clean - @$(MAKE) -C tests -s all - -include Makefile.rocq diff --git a/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg b/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg index e0cc6ba5740d..b61e0ede0928 100644 --- a/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg +++ b/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg @@ -1,3 +1,5 @@ +(** See dev/doc/parsing.md for mlg doc *) + (* -------------------------------------------------------------------------- *) (* *) (* Initial ritual dance *) diff --git a/doc/plugin_tutorial/tuto3/Makefile b/doc/plugin_tutorial/tuto3/Makefile index b042cc842fa0..8fdad97450fd 100644 --- a/doc/plugin_tutorial/tuto3/Makefile +++ b/doc/plugin_tutorial/tuto3/Makefile @@ -1,14 +1,8 @@ -ifeq "$(COQBIN)" "" - COQBIN=$(dir $(shell which rocq))/ -endif +COQBIN?= %: Makefile.rocq Makefile.rocq: _CoqProject $(COQBIN)rocq makefile -f _CoqProject -o Makefile.rocq -tests: all - @$(MAKE) -C tests -s clean - @$(MAKE) -C tests -s all - -include Makefile.rocq diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg index 4d5d9623706f..c8c8c627bfa1 100644 --- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -1,3 +1,5 @@ +(** See dev/doc/parsing.md for mlg doc *) + DECLARE PLUGIN "rocq-plugin-tutorial.tuto3" { diff --git a/doc/plugin_tutorial/tuto4/Makefile b/doc/plugin_tutorial/tuto4/Makefile new file mode 100644 index 000000000000..8fdad97450fd --- /dev/null +++ b/doc/plugin_tutorial/tuto4/Makefile @@ -0,0 +1,8 @@ +COQBIN?= + +%: Makefile.rocq + +Makefile.rocq: _CoqProject + $(COQBIN)rocq makefile -f _CoqProject -o Makefile.rocq + +-include Makefile.rocq diff --git a/doc/plugin_tutorial/tuto4/Makefile.rocq.local b/doc/plugin_tutorial/tuto4/Makefile.rocq.local new file mode 100644 index 000000000000..9117f4984f7a --- /dev/null +++ b/doc/plugin_tutorial/tuto4/Makefile.rocq.local @@ -0,0 +1 @@ +CAMLPKGS := -package rocq-runtime.plugins.ltac2 diff --git a/doc/plugin_tutorial/tuto4/_CoqProject b/doc/plugin_tutorial/tuto4/_CoqProject new file mode 100644 index 000000000000..df23df2756be --- /dev/null +++ b/doc/plugin_tutorial/tuto4/_CoqProject @@ -0,0 +1,10 @@ +src/META.rocq-plugin-tutorial +-R theories Tuto4 +-I src + +theories/Loader.v +theories/Demo.v + +src/myexternals.ml +src/myexternals.mli +src/tuto4_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto4/src/META.rocq-plugin-tutorial b/doc/plugin_tutorial/tuto4/src/META.rocq-plugin-tutorial new file mode 100644 index 000000000000..b3a8259a66b9 --- /dev/null +++ b/doc/plugin_tutorial/tuto4/src/META.rocq-plugin-tutorial @@ -0,0 +1,11 @@ +package "tuto4" ( + directory = "." + version = "dev" + description = "A tuto4 plugin" + requires = "rocq-runtime.plugins.ltac2" + archive(byte) = "tuto4_plugin.cma" + archive(native) = "tuto4_plugin.cmxa" + plugin(byte) = "tuto4_plugin.cma" + plugin(native) = "tuto4_plugin.cmxs" +) +directory = "." diff --git a/doc/plugin_tutorial/tuto4/src/dune b/doc/plugin_tutorial/tuto4/src/dune new file mode 100644 index 000000000000..c9da7899b792 --- /dev/null +++ b/doc/plugin_tutorial/tuto4/src/dune @@ -0,0 +1,4 @@ +(library + (name tuto4_plugin) + (public_name rocq-runtime.plugins.tutorial.p4) + (libraries rocq-runtime.plugins.ltac2)) diff --git a/doc/plugin_tutorial/tuto4/src/myexternals.ml b/doc/plugin_tutorial/tuto4/src/myexternals.ml new file mode 100644 index 000000000000..83df4f9a07a2 --- /dev/null +++ b/doc/plugin_tutorial/tuto4/src/myexternals.ml @@ -0,0 +1,189 @@ +open Names +(* kernel names, ie ModPath, KerName, Id etc *) + +open Ltac2_plugin +(* the Ltac2 plugin is "packaged" ie its modules are all contained in module Ltac2_plugin + without this open we would have to refer to eg Ltac2_plugin.Tac2externals below *) + +open Tac2externals +(* APIs to register new externals, including the convenience "@->" infix operator *) + +open Tac2ffi +(* Translation operators between Ltac2 values and OCaml values in various types *) + +(** **** Two simple examples of tactics *) + +(* Rocq tactics are values of the [Proofview.tactic] monad. + tclUnit in Proofview is the return operation of this monad. + We define an alias for convenience. *) +let return = Proofview.tclUNIT + +(* Used to distinguish our primitives from some other plugin's primitives. + By convention matches the plugin's ocamlfind name. *) +let plugin_name = "rocq-plugin-tutorial.tuto4" + +let pname s = { Tac2expr.mltac_plugin = plugin_name; mltac_tactic = s } + +(* We define for convenience a wrapper around Tac2externals.define. + [define "foo"] has type + [('a, 'b) Ltac2_plugin.Tac2externals.spec -> 'b -> unit]. + Type [('a, 'b) spec] represents a high-level Ltac2 tactic specification. It + indicates how to turn a value of type ['b] into an Ltac2 tactic. + The type parameter ['a] gives the type of value produced by interpreting the + specification. *) +let define s = define (pname s) + +(* We define a tactic taking an Ltac2 integer and returning an Ltac2 boolean + "@->" is an infix function from Tac2externals combining a "type representation" + (Tac2ffi.repr) and a [Tac2externals.spec]. + Here, [int @-> ret bool] means that we want to define an Ltac2 tactic which + takes an Ltac2 int and returns an Ltac2 bool. + [ret] means we return the answer without doing tactic operations + (no access to the Proofview monad). *) +let () = define "the_question" (int @-> ret bool) @@ fun i -> + Int.equal i 42 + +(* Now, we define a wrapper around "exact", it takes a constr + (ie a term) and returns the trivial value (and does side effects on the goal). + "tac" means we have access to the tactic monad. *) +let () = define "my_exact" (constr @-> tac unit) @@ fun c -> + Tactics.exact_check c + +(* We can see our new Ltac2 tactics in action in the beginning of the + theories/Demo.v file. *) + +(** **** Transparent custom type *) + +(* We have seen before how to use the int and bool "reprs" (representations) in Ltac2. + In this section, we will learn to define a "repr" for a custom OCaml type. *) + +(* We define a custom type in OCaml and in Ltac2 (this is the OCaml side): *) +type my_custom = + | A + | B of EConstr.t + (* EConstr.t is the type of terms (it wraps around the kernel + Constr.t to enforce invariants when handling terms with + existential variables). *) + +(* Translate from OCaml to the Ltac2 representation (Tac2val.valexpr). + + Values of Ltac2 algebraic datatypes are represented + + - for constant (without arguments) constructors, by ValInt where + the int is the 0-based index of the constructor (excluding + non-constant constructors) + + - for non-constant (with arguments) constructors, by ValBlk where + the first argument is the 0-based index of the constructor (excluding constant constructors) + and the second is an array containing the arguments. + + eg with [Ltac2 Type foo := [ A | B (x) | C | D (y, z) ]], + - [A] is [ValInt 0] + - [B v] is [ValBlk (0, [|v|])] + - [C] is [ValInt 1] + - [D v1 v2] is [ValBlk (1, [|v1; v2|])] + + When building values from OCaml we can use [of_int] and [of_block] + instead of [ValInt] and [ValBlk]. +*) +let of_custom = function + | A -> of_int 0 + | B c -> + (* Here [of_constr] is [Tac2ffi.of_constr] *) + of_block (0, [|of_constr c|]) + +(* Go from the Ltac2 representation to the OCaml representation. + This needs to look at the low-level valexpr data. + If an external is declared with an incorrect Ltac2 type it may be passed + invalid values, in which case we assert false. *) +let to_custom = let open Tac2val in function + | ValInt 0 -> A + | ValBlk (0, [|c|]) -> + (* [to_constr] is [Tac2ffi.to_constr] *) + B (to_constr c) + | _ -> assert false + + +(* Now we package both translation functions into a Tac2ffi.repr + which is just a record holding these two translation functions *) +let custom = make_repr of_custom to_custom + +(* We can now use custom just like we used the "int" and "bool" reprs before. + For instance, here is a tactic returning true if passed [A] or [B] of some + inductive type. + We need the evar map to inspect the term in the B case, + but we don't need the current goal's hypotheses, so we use "eret" + (in fact we don't use the environment at all). +*) +let () = define "is_ind_or_a" (custom @-> eret bool) @@ fun v env sigma -> + match v with + | A -> true + | B c -> EConstr.isInd sigma c + +(* We can now use custom just like we used the "int" and "bool" reprs before. + For instance, here is a tactic returning true if passed [A] or [B] of some + inductive type. + + We need the evar map to inspect the term in the B case, + but we don't need the current goal's hypotheses, so we use "eret" + (in fact we don't use the environment at all). + + We could also use "gret", but that fails (with an anomaly) when 0 goals are focused. +*) +let () = define "check_in_goal" (ident @-> tac custom) @@ fun id -> + (* pf_apply gives us the "current" environment, ie the global env if + no goals are focused and the current goal env if 1 goal is + focused. If >1 goals are focused it throws an exception. *) + Tac2core.pf_apply @@ fun env sigma -> + match EConstr.lookup_named id env with + | exception Not_found -> return A + | d -> return (B (Context.Named.Declaration.get_type d)) + +(* **** Abstract custom type *) + +(* Now we define a custom type in OCaml, but we do not want to expose its + representation in Ltac2. *) +type custom2 = int * int + +(* The string given to Val.create must be GLOBALLY unique (not just unique to the current plugin). + If we wanted to be safe we could do [create (plugin_name^":mycustom2")]. *) +let val_custom2 = Tac2dyn.Val.create "mycustom2" + +(* the "repr" for our custom values *) +let custom2 = repr_ext val_custom2 + +(* a couple toy functions *) +let () = define "mk_custom2" (int @-> int @-> ret custom2) @@ fun i j -> + (i, j) + +let () = define "sum2" (custom2 @-> ret int) @@ fun (i,j) -> + i + j + +(* we can also declare a printer for our custom values. *) + +(* Ltac2 printers are type-directed, so we need to tell which type we know how to print. + The type is identified by its nma of type [Tac2expr.type_constant = KerName.t]. + Current APIs for this are not very nice, we have to write module paths by hand. *) + +(* the loader module is a file whose logical name is Tuto4.Loader *) +let loader_module_name = ModPath.MPfile (DirPath.make @@ List.map Id.of_string ["Loader"; "Tuto4"]) + +(* the type in that module is "custom2" *) +let custom2_type_name = KerName.make loader_module_name (Label.of_id @@ Id.of_string "custom2") + +(* the printing system gives us the current env and evar map, the + value to be printed, and the type arguments at which we are printing. *) +let pr_custom2 env sigma v tys = + assert (CList.is_empty tys); (* Since custom2 has no arguments, tys is the empty list. *) + (* by typing, v must be a custom2 value *) + let (i, j) = repr_to custom2 v in + (* NB: open Pp would shadow "v" if we did it between binding "v" and using it *) + let open Pp in + int i ++ str "," ++ int j + +(* Finally, we register our printer for custom2 to be used in Ltac2. + It will be used every time Ltac2 needs to output values of type custom2. *) +let () = Tac2print.register_val_printer custom2_type_name { val_printer = pr_custom2 } + +(* The end of Demo.v show how Ltac2 will use this printer function + whenever it needs to print a value of type custom2. *) diff --git a/doc/plugin_tutorial/tuto4/src/myexternals.mli b/doc/plugin_tutorial/tuto4/src/myexternals.mli new file mode 100644 index 000000000000..c1a1384d969e --- /dev/null +++ b/doc/plugin_tutorial/tuto4/src/myexternals.mli @@ -0,0 +1,9 @@ +open Ltac2_plugin +open Tac2ffi + +(** We don't need to expose any APIs for the plugin to work, but we + may if we want to allow further plugins to build on this one. *) + +type custom2 + +val custom2 : custom2 repr diff --git a/doc/plugin_tutorial/tuto4/src/tuto4_plugin.mlpack b/doc/plugin_tutorial/tuto4/src/tuto4_plugin.mlpack new file mode 100644 index 000000000000..4edfe8e35d40 --- /dev/null +++ b/doc/plugin_tutorial/tuto4/src/tuto4_plugin.mlpack @@ -0,0 +1 @@ +Myexternals diff --git a/doc/plugin_tutorial/tuto4/theories/Demo.v b/doc/plugin_tutorial/tuto4/theories/Demo.v new file mode 100644 index 000000000000..e4cf599c3311 --- /dev/null +++ b/doc/plugin_tutorial/tuto4/theories/Demo.v @@ -0,0 +1,28 @@ +From Ltac2 Require Import Ltac2. +From Tuto4 Require Import Loader. + +(* try out our "question" primitive *) +Ltac2 Eval question 2. (* false *) +Ltac2 Eval question 42. (* true *) + +(* try out our "tuto_exact" primitive *) +Goal True. + Fail tuto_exact '0. + tuto_exact 'I. +Qed. + +(* try out our custom type functions *) +Ltac2 Eval ind_or_a A. +Ltac2 Eval ind_or_a (B '0). +Ltac2 Eval ind_or_a (B 'nat). + +Goal nat -> nat. + intros x. + Ltac2 Eval check_in_goal @x. + Ltac2 Eval check_in_goal @y. +Abort. + +(* try out our custom2 functions *) +Ltac2 Eval mk_custom2 2 4. (* our printer works *) + +Ltac2 Eval sum2 (mk_custom2 2 4). diff --git a/doc/plugin_tutorial/tuto4/theories/Loader.v b/doc/plugin_tutorial/tuto4/theories/Loader.v new file mode 100644 index 000000000000..1ad59764a7b2 --- /dev/null +++ b/doc/plugin_tutorial/tuto4/theories/Loader.v @@ -0,0 +1,35 @@ +From Ltac2 Require Import Ltac2. + +Declare ML Module "rocq-plugin-tutorial.tuto4". + +(** A simple function taking an integer and returning a boolean. + Note that the internal name "the_question" does not need to match the exposed name "question". *) +Ltac2 @external question : int -> bool + := "rocq-plugin-tutorial.tuto4" "the_question". + +(** a wrapper around "exact" *) +Ltac2 @external tuto_exact : constr -> unit + := "rocq-plugin-tutorial.tuto4" "my_exact". + +(** Some custom type. *) +Ltac2 Type custom := [ A | B (constr) ]. + +(** A function returning true if passed [A] or [B] of some inductive type. *) +Ltac2 @external ind_or_a : custom -> bool + := "rocq-plugin-tutorial.tuto4" "is_ind_or_a". + +(** a function returning [A] if the ident is not an hypothesis, + or [B t] where [t] is its type if it is. *) +Ltac2 @external check_in_goal : ident -> custom + := "rocq-plugin-tutorial.tuto4" "check_in_goal". + +(** Another custom type, this one abstract on the Ltac2 side. *) +Ltac2 Type custom2. + +(** Build a custom2 value. *) +Ltac2 @external mk_custom2 : int -> int -> custom2 + := "rocq-plugin-tutorial.tuto4" "mk_custom2". + +(** Get something from a custom2 value. *) +Ltac2 @external sum2 : custom2 -> int + := "rocq-plugin-tutorial.tuto4" "sum2". diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index 76c45b3004b0..30b9c0681ac4 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -137,13 +137,12 @@ margin-top: 0.5em !important; } -.coqdoc, .coqtop dl { +.coqdoc > span, .coqtop dl { margin: 12px; /* Copied from RTD theme */ } -.coqdoc { +.coqdoc > span { display: block; - white-space: pre; } .coqtop dt, .coqtop dd { @@ -156,7 +155,7 @@ } /* FIXME: Specific to the RTD theme */ -.coqdoc, .coqtop dt, .coqtop dd, pre { /* pre added because of production lists */ +.coqdoc > span, .coqtop dt, .coqtop dd, pre { /* pre added because of production lists */ font-family: Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace !important; /* Copied from RTD theme */ font-size: 12px !important; /* Copied from RTD theme */ line-height: 1.5 !important; /* Copied from RTD theme */ @@ -281,3 +280,8 @@ code span.error { padding-left: 2em; /* indent 2nd & subsequent lines */ text-indent: -2em; } + +.rst-content dl:not(.docutils) dt { + padding: 6px; + display: table; +} diff --git a/doc/sphinx/addendum/rewrite-rules.rst b/doc/sphinx/addendum/rewrite-rules.rst index 2c188ef7700f..4f27b68681f0 100644 --- a/doc/sphinx/addendum/rewrite-rules.rst +++ b/doc/sphinx/addendum/rewrite-rules.rst @@ -128,7 +128,7 @@ Universe polymorphic rules -------------------------- Rewrite rules support universe and sort quality polymorphism. -Universe levels and sort quality variables must be declared with the notation :n:`@{q1 q2|u1 u2+|+}` +Universe levels and sort quality variables must be declared with the notation :n:`@{q1 q2;u1 u2+|+}` (the same notation as universe instance declarations); each variable must appear exactly once in the pattern. If any universe level isn't bound in the rule, @@ -141,9 +141,9 @@ so all inferred constraints from the left-hand side are used for the replacement .. rocqtop:: reset all warn - #[universes(polymorphic)] Symbol raise@{q|u|} : forall (A : Type@{q|u}), A. + #[universes(polymorphic)] Symbol raise@{q;u} : forall (A : Type@{q;u}), A. Rewrite Rule raise_nat := - @{q|u+|+} |- raise@{q|u} (forall (x : ?A), ?P) => fun (x : ?A) => raise@{q|u} ?P. + @{q;u+|+} |- raise@{q;u} (forall (x : ?A), ?P) => fun (x : ?A) => raise@{q;u} ?P. Rewrite rules, type preservation, confluence and termination ------------------------------------------------------------ diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 207e52ffa8d7..7cc6e049198b 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -28,7 +28,7 @@ Rocq program or by turning the :flag:`Allow StrictProp` flag off. :undocumented: Some of the definitions described in this document are available -through ``Stdlib.Logic.StrictProp``, which see. +through ``Stdlib.Logic.StrictProp``. Basic constructs ---------------- diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 4400ace98b09..6fa4c3aab20f 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -281,7 +281,7 @@ The following is an example of a record with non-trivial subtyping relation: .. math:: - E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} + E[Γ] ⊢ \mathsf{packType}@\{i\} ≤_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j Looking back at the example of monoids, we can see that they are naturally @@ -605,7 +605,7 @@ Printing universes The :n:`Subgraph` clause limits the printed graph to the requested names (adjusting constraints to preserve the implied transitive constraints between kept universes). :n:`@debug_univ_name` is - `:n:`@qualid` for named universes (e.g. `eq.u0`), and :n:`@string` + :n:`@qualid` for named universes (e.g. `eq.u0`), and :n:`@string` for raw universe expressions (e.g. `"Stdlib.Init.Logic.1"`). By default when printing a subgraph `Print Universes` attempts to @@ -818,7 +818,7 @@ bound variable. Instantiating `s` in `Type@{s;u}` with the impredicative `Prop` or `SProp` produces `Prop` or `SProp` respectively regardless of the -instantiation fof `u`. +instantiation of `u`. .. rocqtop:: all diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index bd43468042ea..db7eb69acf79 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8,6 +8,520 @@ Recent changes .. include:: ../unreleased.rst +Version 9.1 +----------- + +.. contents:: + :local: + :depth: 1 + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +We highlight some of the most impactful changes here: + +- fixed incorrect guard checking leading to inconsistencies (multiple PRs) + +- sort polymorphic universe instances :ref:`should now be written <91sortpolysyntax>` + as `@{s ; u}` instead of `@{s | u}` + +- :ref:`fixed <91ltac2notationfix>` handling of notation variables for ltac2 in notations + (i.e. `Notation "'foo' x" := ltac2:(...)`) + +- :ref:`Support <91refinedef>` for :attr:`refine` attribute in :cmd:`Definition` + +- Rocq can be compile-time configured to be :ref:`relocatable <91relocatable>` + +- extraction :ref:`handles <91extractsortpoly>` sort polymorphic definitions + +See the `Changes in 9.1.0`_ section below for the detailed list of changes, +including potentially breaking changes marked with **Changed**. +Rocq's `reference manual for 9.1 `_, +documentation of the 9.1 `corelib `__ +and `developer documentation of the 9.1 ML API `_ +are also available. + +Théo Zimmermann, with help from Jason Gross and Gaëtan Gilbert, maintained +`coqbot `__ used to run Rocq's CI and other +pull request management tasks. + +Jason Gross maintained the `bug minimizer `_ +and its `automatic use through coqbot `__. + +Ali Caglayan, Emilio Jesús Gallego Arias, Rudi Grinberg and Rodolphe Lepigre maintained the +`Dune build system for OCaml and Coq/Rocq `_ +used to build the Rocq Prover itself and many Rocq projects. + +The `opam repository `_ for Rocq packages has been maintained by +Guillaume Claret, Guillaume Melquiond, Karl Palmskog, Matthieu Sozeau +and Enrico Tassi with contributions from many users. The up-to-date list +of packages is `available on the Rocq website `_. + +Erik Martin-Dorel maintained the +`Rocq Docker images `_ and +the `docker-keeper `_ compiler +used to build and keep those images up to date (note that the tool is not Rocq specific). +Erik Martin-Dorel and Théo Zimmermann maintained the +`docker-coq-action `_ +container action (which is applicable to any opam project hosted on GitHub). + +Cyril Cohen, Vincent Laporte, Pierre Roux and Théo Zimmermann +maintained the `Nix toolbox `_. +The docker-coq-action and the Nix toolbox are used by many Rocq projects for continuous integration. + +Rocq 9.1 was made possible thanks to the following 24 reviewers: +Florian Angeletti, Ali Caglayan, Cyril Cohen, Pierre Courtieu, Jim +Fehrle, Gaëtan Gilbert, Jason Gross, Emilio Jesús Gallego Arias, +Jan-Oliver Kaiser, Thomas Lamiaux, Rodolphe Lepigre, +Erik Martin-Dorel, Guillaume Melquiond, Patrick Nicodemus, +Pierre-Marie Pédrot, Pierre Rousselin, Pierre Roux, Gabriel Scherer, +Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi, Théo Winterhalter and +Théo Zimmermann. + +See the `Rocq Team `_ page for +more details on Rocq's development teams. + +The 45 contributors to the 9.1 version are: Soudant, +ypopovitch, Reynald Affeldt, Wassim Ait-Moussa, David Allsopp, +Christian Benedict Smit, Frédéric Besson, Mathis Bouverot, Ali +Caglayan, Jean Caspar, Benedict Christian Smit, Cyril Cohen, Pierre Courtieu, +Julien Cretin, Jian Fang, Jim Fehrle, Gaëtan Gilbert, Jason Gross, +Dario Halilovic, Hugo Herbelin, Elyes Jemel, Emilio Jesús Gallego +Arias, Jan-Oliver Kaiser, Kacper Korban, Lucie Lahaye, Thomas Lamiaux, +Rodolphe Lepigre, Yann Leray, Kenji Maillard, Erik Martin-Dorel, +Patrick Nicodemus, Charles Norton, Pim Otte, Pierre-Marie Pédrot, +Josselin Poiret, Johann Rosain, Pierre Rousselin, Pierre Roux, +Radosław Rowicki, Benedict Smit, Bastien Sozeau, Matthieu Sozeau, +Nicolas Tabareau, Enrico Tassi and Théo Zimmermann. + +The Rocq community at large helped improve this new version via +the GitHub issue and pull request system, +the `Discourse forum `__ and the +`Rocq Zulip chat `_. + +Gaëtan Gilbert and Pierre-Marie Pédrot are the release managers of Rocq 9.1. +This release is the result of 397 merged PRs, closing 56 issues. + +| Nantes, September 2025 +| Gaëtan Gilbert and Pierre-Marie Pédrot for the Rocq development team + +Changes in 9.1.0 +~~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +Kernel +^^^^^^ + +- **Fixed:** + Guard checking forgot to check non principal arguments of a fixpoint + for unguarded uses of the fixpoint leading to an inconsistency + (`#20415 `_, + fixes `#20413 `_, + by Gaëtan Gilbert). +- **Fixed:** + inconsistency from incomplete guard checking with nested matches + (`#20457 `_, + fixes `#20455 `_, + by Gaëtan Gilbert). +- **Fixed:** + inconsistency from incorrect reduction across a fixpoint during guard checking + (`#20648 `_, + fixes `#20555 `_, + by Yann Leray). +- **Fixed:** + Wrong context management during rewrite rule reduction + (`#20729 `_, + fixes `#20728 `_, + by Yann Leray). +- **Fixed:** + Fix guard checker making propositional extensionality inconsistent + (`#21050 `_, + fixes `#21053 `_, + by Yann Leray). +- **Fixed:** + substitution of functor delta-resolvers when strengthening. + The previous code was only substituting the inner delta resolvers + and ignoring the codomain of functors. In particular this was generating + ill-formed constants whose canonical component was pointing to a bound name + that did not exist in the global environment, leading to an inconsistency + (`#21057 `_, + fixes `#21051 `_, + by Pierre-Marie Pédrot). + +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +.. _91sortpolysyntax: + +- **Deprecated:** + in :ref:`sort polymorphic ` instances, separating sorts from universes using `|` instead of `;` (the later being possible since this version) + (`#20635 `_, + by Gaëtan Gilbert). +- **Added:** + in :ref:`sort polymorphic ` instances, sorts can be separated from universes using `;` instead of `|`. + This is less ambiguous as `|` is also used to separate universes and constraints when declaring sort polymorphic objects, + and in such declarations when constraints are unspecified it allows omitting the `|` + (`Definition foo@{s;u} := ...` instead of `Definition foo@{s|u|+} := ...`) + (`#20635 `_, + by Gaëtan Gilbert). +- **Fixed:** + Anomaly `List.chop` in the presence of projections with not + enough argument scopes (`#20945 + `_, fixes `#20940 + `_, by Hugo + Herbelin). +- **Fixed:** + Anomaly `List.chop` with too many projection parameters in an abbreviation + (`#20946 `_, + fixes `#15815 `_, + by Hugo Herbelin). + +Notations +^^^^^^^^^ + +- **Changed:** + The `Specif` notations (`exists x : A, P`, `{ x : A | P }`, `{ x : A & P }`, etc) + locally opens `type_scope` for the second component (`P`). + This makes eg `{ x & type_1 * type_2 }` work even when `nat_scope` is opened instead of interpreting `*` as peano multiplication + (`#20294 `_, + by Gaëtan Gilbert). +- **Changed:** + :cmd:`Enable Notation` and :cmd:`Disable Notation` do not take + effect in deep imports (i.e. when a parent of their origin module is + imported) + (`#20484 `_, + by Gaëtan Gilbert). + +Tactics +^^^^^^^ + +- **Changed:** + the :tacn:`abstract` tactic now only registers a name + for the sublemma after the whole tactic block has run, + i.e. after a dot. In particular, the sublemma cannot + be accessed by its name while the tactic call has not + returned + (`#14937 `_, + by Pierre-Marie Pédrot). +- **Changed:** + the congruence tactic now can handle some dependently typed constructor fields. + The field's type has to be composed of terms occuring globally or projectable from + parameters or indices of the inductive type + (`#19700 `_, + by Benedict Christian Smit). +- **Changed:** + setoid rewriting now rewrites under primitive projections. + In rare cases (see for instance + `#20575 `_), + some rewrite that used to accidentally work will now correctly fail + (`#19811 `_, + by Josselin Poiret and Pierre-Marie Pédrot). +- **Changed:** + output of :cmd:`Print Instances` better matches the actual behaviour + when an instance is declared multiple times with different priorities + (`#20486 `_, + by Gaëtan Gilbert). +- **Added:** + a new :flag:`Rewrite Output Constraints` flag and :ref:`documented ` its use + for debugging typeclass resolution failures in setoid rewriting + (`#20476 `_, + by Matthieu Sozeau). + +Ltac language +^^^^^^^^^^^^^ + +- **Changed:** + :cmd:`Ltac` redefinitions (`Ltac ::=`) understand :attr:`export`. + Previously :attr:`global` and the default locality meant the redefinition would + take effect at Require time and when importing any surrounding module. + Now :attr:`global` means it takes affect at Require time, + :attr:`export` when the current module (but not its parents) is imported, + and the default is equivalent to the combination of :attr:`global` and :attr:`export` + (`#20054 `_, + by Gaëtan Gilbert). +- **Changed:** + :cmd:`Ltac` redefinitions (`Ltac foo ::= ...`) are not undone by + importing the module containing the original definition. + To get the previous behaviour, add `Ltac foo ::= orig_def.` + after the original definition `Ltac foo := orig_def.` + (`#20391 `_, + by Gaëtan Gilbert). +- **Changed:** + Named goals can now appear in any goal selector list + (`#20511 `_, + fixes `#12838 `_, + by Dario Halilovic). + +Ltac2 language +^^^^^^^^^^^^^^ + +- **Changed:** + Ltac2 does not depend on the prelude (i.e. it is compiled with `-noinit`). + It still depends on `Corelib.Init.Ltac` due to the interoperation with Ltac1 + (`#20387 `_, + by Gaëtan Gilbert). +- **Changed:** + the documentation and error messages do not use the term "scope" to describe Ltac2 :ref:`syntactic_classes` + (`#20504 `_, + by Gaëtan Gilbert). +- **Changed:** + :cmd:`Ltac2 Set` only takes effect with shallow imports, i.e. + `Import Foo` will not run a mutation from (non exported) inner module `Foo.Bar` + (`#20516 `_, + by Gaëtan Gilbert). +- **Added:** + A file `Ltac1CompatNotations` for Ltac2 Notations reproducing Ltac1 parsing of tactics, + that can be harmful to parsing, and produce bad error messages. + (`#20569 `_, + by Thomas Lamiaux). +- **Added:** + `rename` (in `Ltac1CompatNotations`), `eassumption`, `cycle`, and `exfalso` Ltac2 notations + (`#20197 `_, + by Josselin Poiret). +- **Added:** + ``Ltac2.Constr.is_string``, ``Ltac2.Constr.is_sort`` + (`#20088 `_, + by Jason Gross). +- **Added:** + ``Ltac2.Constr.decompose_app_list``, ``Ltac2.Constr.decompose_app`` + (`#20089 `_, + by Jason Gross). +- **Added:** + ``Ltac2.Option.is_some``, ``Ltac2.Option.is_none``, ``Ltac2.Option.compare``, + ``Ltac2.Option.join``, ``Ltac2.Option.iter`` + (`#20184 `_, + by Jason Gross). +- **Added:** + `empty` and `add` in `Ltac2.Fresh.Free`, `next` in `Ltac2.Fresh`. + `Ltac2.Fresh` operations should also be faster + (`#20220 `_, + by Gaëtan Gilbert). +- **Added:** + Enable use of (open\_)lconstr inside Ltac2 Notation command + (`#20430 `_, + by Pim Otte). +- **Added:** + API functions for inductive types - `Ind.nparams`, `Ind.nparams_uniform`, `Ind.constructor_nargs`, `Ind.constructor_ndecls`, `Constr.Case.inductive` + (`#20475 `_, + fixes `#10940 `_, + by Patrick Nicodemus). +- **Added:** + format specifiers `%A` to use unthunked printers and `%m` for already-formatted messages. + Typically, instead of `printf "foo: %a" (fun () v => print_thing v) v` + we can now write `printf "foo: %A" print_thing v` + or `printf "foo: %m" (print_thing v)` + (`#20498 `_, + by Gaëtan Gilbert). +- **Added:** + Ltac2 type for reduction expressions + (`#20543 `_, + by Radosław Rowicki, with review of Pierre-Marie Pédrot and Gaëtan Gilbert and Jason Gross). +- **Added:** + Ported `rewrite_strat` to Ltac2 and added the `Rewrite.Strategy` module for describing rewrite strategies + (`#20544 `_, + fixes `#20482 `_, + by Radosław Rowicki with review of Jason Gross and Pierre-Marie Pédrot and Gaëtan Gilbert). +- **Added:** + ``Ltac2.Message.empty`` + (`#20547 `_, + by Elyes Jemel). +- **Added:** + conversion tests to Unification - `Unification.conv`, `Unification.conv_current`, `Unification.conv_full` + (`#20649 `_, + fixes `#20579 `_, + by Thomas Lamiaux). +- **Added:** + antiquotation `$hyp:id` in terms for dynamically named hypotheses, + i.e. `let x := @y in constr:($hyp:x)` is equivalent to `constr:(&y)` + (`#20656 `_, + by Gaëtan Gilbert). + +.. _91ltac2notationfix: + +- **Fixed:** + Ltac2 in terms in notations is more aware of the notation variables it uses, + providing early failure when the variable is instantiated with an invalid term, + preventing a spurious warning when a variable that cannot be instantiated is unused, + and preventing exponential blowups from copying unused data + (`#20313 `_, + fixes `#17833 `_ + and `#20188 `_ + and `#20305 `_, + by Gaëtan Gilbert). + +SSReflect +^^^^^^^^^ + +- **Changed:** + `%FUN` now delimits scope `function_scope` rather than `fun_scope` + in `ssrfun.v` + (`#20478 `_, + by Pierre Roux). +- **Removed:** + scope `fun_scope` from `ssrfun.v` that was deprecated since 8.20, + use `function_scope` instead + (`#20478 `_, + by Pierre Roux). +- **Deprecated:** + `idempotent` in `ssrfun.v`, use `idempotent_op` instead + (`#20478 `_, + by Pierre Roux). +- **Added:** + definitions `injective2`, `idempotent_op` and `idempotent_fun` and + lemmas `omap_id`, `eq_omap`, `inj_omap`, `omapK`, `inr_inj` and + `inl_inj` in `ssrfun.v` + (`#20478 `_, + by Pierre Roux). + +Commands and options +^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + commands taking a tactic argument (e.g. :cmd:`Hint Extern`) + now follow :opt:`Default Proof Mode` instead of hardcoding Ltac1 + (`#19690 `_, + fixes `#13784 `_, + by Gaëtan Gilbert). +- **Changed:** + :opt:`Printing Depth` completely skips subterms beyond the given depth. + In general the formatter depth is higher than the term depth, so there is no visible change, + but some notations print subterms without increasing the formatting depth in which case + you may need to increase the printing depth to avoid `...` + (`#20275 `_, + by Gaëtan Gilbert). +- **Changed:** + :cmd:`Search` ignores lemmas declared with :attr:`local` unless + new flag :flag:`Search Blacklist Locals` is unset + (`#20349 `_, + by Gaëtan Gilbert). +- **Changed:** + :cmd:`Search` now accepts open modules, including the current file with + the `in`, `inside` and `outside` filters. + (`#20733 `_, + fixes `#14010 `_, + by Pierre Rousselin, with a lot of help by Gaëtan Gilbert). +- **Removed:** + flag `Lia Enum`, which did nothing + (`#20640 `_, + by Gaëtan Gilbert). +- **Added:** + :cmd:`Sort` to declare global or section-scoped sort qualities + (`#18615 `_, + by Kenji Maillard). +- **Added:** + :cmd:`Number Notation` and :cmd:`String Notation` understand parsers which may produce error messages + (`#20107 `_, + fixes `#20042 `_, + by Gaëtan Gilbert). + +.. _91refinedef: + +- **Added:** + support for the :attr:`refine` attribute to definitions and (co)fixpoints + (`#20355 `_, + fixes `#20302 `_, + by Yann Leray). + +Command-line tools +^^^^^^^^^^^^^^^^^^ + +- **Changed:** + `rocq timelog2html` now needs package `rocq-devtools` to be installed + (`#20169 `_, + by Gaëtan Gilbert). +- **Added:** + error on ambiguous :cmd:`Require`. Rocq used to silently select a file + when ambiguous :cmd:`Require`\s came from different loadpaths, for instance + different fields of the ``ROCQPATH`` environment variable + (`#20601 `_, + fixes `#20587 `_, + by Gaëtan Gilbert). +- **Fixed:** + `rocq dep` implicitly adds `-I $rocq-runtime/..` after the explicit `-I` instead of before + (where `$rocq-runtime` is the expected location of the rocq-runtime package). + This means that if a local plugin (whose META is in an explicit `-I` path) is installed next to rocq-runtime, + `rocq dep` will emit a dependency on the local version instead of the installed version + (`#20393 `_, + by Gaëtan Gilbert). + +RocqIDE +^^^^^^^ + +- **Changed:** + default character encoding is UTF8 (it was locale dependent on non-windows OSes), + and when the configured encoding is not UTF8 RocqIDE will attempt to convert input files even if they are already valid UTF8 + (`#20256 `_, + fixes `#11526 `_, + by Gaëtan Gilbert). +- **Added:** + an option to control the maximum length of the message view + in RocqIDE + (`#20597 `_, + fixes `#20420 `_, + by Pierre-Marie Pédrot). + +Corelib +^^^^^^^ + +- **Added:** + type `result` in `Corelib.Datatypes`, equivalent to `sum` + but with a name fitting possibly-failing computations + (`#20107 `_, + by Gaëtan Gilbert). + +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + minimum supported OCaml version is now 4.14.0 (instead of 4.09.0), + and minimum supported OCamlfind version is now 1.9.1 (instead of 1.8.1) + (`#20576 `_, + by Gaëtan Gilbert). + +.. _91relocatable: + +- **Added:** + Rocq can be compile-time configured to be relocatable, + using `./configure -relocatable` instead of e.g. `./configure -prefix /some/path`. + See :ref:`system_config` for an explanation of how Rocq uses its configured installation paths + (`#19901 `_, + by Gaëtan Gilbert). +- **Added:** Experimental support for native Windows builds. + Rocq can now build and run under a native Windows environment using + the new native Windows support in Opam 2.3. This setup is tested in + CI, running a large part of the test suite. Beware this support is + still experimental, and some problem may arise on Unix-specific + tools. Note that RocqIDE is still not supported (c.f. `#20631 + `_) (`#20464 + `_, by Emilio Jesus + Gallego Arias, Gaëtan Gilbert, David Allsopp, Ali Caglayan, Jason + Gross, the Opam team, the @setup-ocaml team, the OCaml team). +- **Fixed:** + Bad interaction between dune, `rocq dep`, and local opam directory switches + (`#20437 `_, + fixes `#20422 `_, + by Rodolphe Lepigre). + +Extraction +^^^^^^^^^^ + +.. _91extractsortpoly: + +- **Fixed:** + extraction handles sort polymorphic definitions + (`#20655 `_, + by Pierre-Marie Pédrot). + +Miscellaneous +^^^^^^^^^^^^^ + +- **Added:** + plugin tutorial for extending Ltac2 + (`#20670 `_, + by Gaëtan Gilbert). + Version 9.0 ----------- diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f56fc49141c8..1024fc81fb55 100644 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -112,7 +112,7 @@ def setup(app): # General information about the project. project = 'The Rocq Prover' -copyright = '1999-2024, Inria, CNRS and contributors' +copyright = '1999-2025, Inria, CNRS and contributors' author = 'The Rocq Development Team' # The version info for the project you're documenting, acts as replacement for @@ -213,6 +213,7 @@ def setup(app): 'versions': [ ("dev", "https://rocq-prover.org/doc/master/refman/"), ("stable", "https://rocq-prover.org/refman/"), + ("9.1", "https://rocq-prover.org/doc/v9.1/refman/"), ("9.0", "https://rocq-prover.org/doc/v9.0/refman/"), ("8.20", "https://rocq-prover.org/doc/V8.20.1/refman/"), ("8.19", "https://rocq-prover.org/doc/V8.19.2/refman/"), diff --git a/doc/sphinx/dune b/doc/sphinx/dune.disabled similarity index 100% rename from doc/sphinx/dune rename to doc/sphinx/dune.disabled diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 72d1c095072a..5bbc3d3839fd 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -358,6 +358,8 @@ rest of the Rocq Prover manual: :term:`terms ` and :term:`types :term:`tactics `. For example: ``split`` is a simple tactic while ``split; auto`` combines two simple tactics. + For more information, see :ref:`compil-steps`. + command A :production:`command` can be used to modify the state of a Rocq diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 4d115c8f68cd..0843981c2108 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -79,6 +79,8 @@ describes tactics that only apply conversion rules. (Other tactics may use conversion rules in addition to other changes to the proof state.) +.. _alpha-conversion-sect: + α-conversion ~~~~~~~~~~~~ @@ -88,6 +90,8 @@ For example `forall x, x + 0 = x` is α-convertible with `forall y, y + 0 = y`. (Internally, Rocq represents these two terms using de Bruijn indices, so explicit α-conversion is not necessary.) +.. _beta-reduction-sect: + β-reduction ~~~~~~~~~~~ @@ -145,6 +149,8 @@ or :term:`constants ` defined in the :term:`global environment` with t marked :gdef:`transparent`. :gdef:`Opaque ` is the opposite of transparent; :term:`delta-reduction` doesn't unfold opaque constants. +.. _iota-reduction-sect: + ι-reduction ~~~~~~~~~~~ @@ -156,6 +162,8 @@ constructor behaves as expected. This reduction is called :gdef:`ι-reduction ` and is more precisely studied in :cite:`Moh93,Wer94`. +.. _zeta-reduction-sect: + ζ-reduction ~~~~~~~~~~~ diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index f3352ed3d3e3..75e6fdd72a93 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -22,7 +22,7 @@ Defining record types .. prodn:: record_definition ::= {? > } @ident_decl {* @binder } {? : @sort } {? := {? @ident } %{ {? {+; @record_field } {? ; } } %} {? as @ident } } - record_field ::= {* #[ {+, @attribute } ] } @name {? @field_spec } {? %| @natural } + record_field ::= {* #[ {+, @attribute } ] } @name {? @field_spec } {? %| @natural } {? @decl_notations } field_spec ::= {* @binder } @of_type_inst | {* @binder } := @term | {* @binder } @of_type_inst := @term @@ -86,19 +86,11 @@ Defining record types :n:`| @natural` Specifies the priority of the field. It is only allowed in :cmd:`Class` commands. - :n:`:` - Specifies the type of the field. - - :n:`:>` - If specified, the field is declared as a coercion from the record name - to the class of the field type. See :ref:`coercions`. - - :n:`::` - If specified, the field is declared a typeclass instance of the class - of the field type. See :ref:`typeclasses`. - - :n:`::>` - Acts as a combination of :n:`::` and :n:`:>`. + :n:`{? @decl_notations }` + Defines notations that are active in subsequent fields, not in the field + itself, until the end of the :cmd:`Record` (see :ref:`example + `). Note that :g:`where` clauses cannot be added at + the record level. - :n:`{+ @binder } : @of_type_inst` is equivalent to :n:`: forall {+ @binder } , @of_type_inst` @@ -113,6 +105,20 @@ Defining record types on the fields that appear before it. Since their values are already defined, such fields cannot be specified when constructing a record. + :n:`:` + Specifies the type of the field. + + :n:`:>` + If specified, the field is declared as a coercion from the record name + to the class of the field type. See :ref:`coercions`. + + :n:`::` + If specified, the field is declared a typeclass instance of the class + of the field type. See :ref:`typeclasses`. + + :n:`::>` + Acts as a combination of :n:`::` and :n:`:>`. + The :cmd:`Record` command supports the :attr:`universes(polymorphic)`, :attr:`universes(template)`, :attr:`universes(cumulative)`, :attr:`private(matching)` and :attr:`projections(primitive)` attributes. @@ -177,6 +183,27 @@ Defining record types Class MyClass := { myfield2 : nat }. About myfield2. (* Argument name defaults to the class name and is marked implicit *) +.. _record_where_clause: + + .. example:: Using a :g:`where` clause in a record field + + .. rocqtop:: all + + Reserved Notation "a & b" (at level 40, left associativity). + Record nat_comoid := + { + op : nat -> nat -> nat where "a & b" := (op a b); + identity : nat; + identity_cond : forall n, identity & n = n; + comm: forall a b, a & b = b & a; + assoc: forall a b c, a & (b & c) = a & b & c + }. + + .. exn:: Error: "where" clause not supported for records. + + :g:`where` clauses are only supported for :n:`@record_field`\s, not for the overall + record definition. + .. exn:: Records declared with the keyword Record or Structure cannot be recursive. The record name :token:`ident` appears in the type of its fields, but uses diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index 07f1142b1d89..4c29c4d70b10 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -246,7 +246,7 @@ A similar table for :cmd:`Module` can be found .. [#note1] For :cmd:`Definition`, :cmd:`Lemma`, ... the default visibility is to be available outside the section and available with a short name when the - current :cmd:`Module` is imported (with :cmd:`Import` or cmd:`Export`) + current :cmd:`Module` is imported (with :cmd:`Import` or :cmd:`Export`) outside the current :cmd:`Module`. The :attr:`local` attribute make the corresponding identifiers available in the current :cmd:`Module` but only with a fully qualified name outside the @@ -255,14 +255,14 @@ A similar table for :cmd:`Module` can be found .. [#note2] For :cmd:`Coercion` and :cmd:`Canonical Structure`, the :attr:`global` visibility, which is the default, makes them available outside the section, in the current :cmd:`Module`, and outside the current - :cmd:`Module` when it is imported (with :cmd:`Import` or cmd:`Export`). + :cmd:`Module` when it is imported (with :cmd:`Import` or :cmd:`Export`). .. [#note3] For :cmd:`Set` and :cmd:`Unset`, the :attr:`export` and :attr:`global` attributes both make the command's effects persist outside the current section, in the current :cmd:`Module`. It will also persist outside the current :cmd:`Module` with the :attr:`global` attribute, or with the :attr:`export` attribute, when the - :cmd:`Module` is imported (with :cmd:`Import` or cmd:`Export`). + :cmd:`Module` is imported (with :cmd:`Import` or :cmd:`Export`). The default behaviour (no attribute) is to make the setting persist outside the section in the current :cmd:`Module`, but not outside the current :cmd:`Module`. diff --git a/doc/sphinx/language/extensions/compil-steps.rst b/doc/sphinx/language/extensions/compil-steps.rst new file mode 100644 index 000000000000..cf2f7695b4ba --- /dev/null +++ b/doc/sphinx/language/extensions/compil-steps.rst @@ -0,0 +1,170 @@ +.. _compil-steps: + +======================== +Command level processing +======================== + +When a command, for instance :g:`Check 1 + 2 * 2.` is fed to Rocq, it +goes through several *successive* processing steps: + +* :term:`lexing` splits the input string into a sequence of tokens ; +* :term:`parsing` converts the sequence of tokens into a syntax tree ; +* :term:`synterp` does just enough to be able to proceed parsing the + file (that is, executes the few commands that can modify the lexer + or parser) ; +* :term:`interp` executes the bulk of the parsed commands. + +.. note:: + + Understanding the distinction between lexing and parsing is + sometimes required to make good use of the notation features. + The synterp/interp distinction, while important for developers, + should be mostly transparent for users. + +Lexing +~~~~~~ + +The first step, :gdef:`lexing` splits the input into a sequence of +tokens, for instance the string ``"Check 1 + 2 * 2."`` is split into +the sequence of seven tokens `'Check' '1' '+' '2' '*' '2' '.'`. A set +of :ref:`basic tokens ` are predefined and can be +extended, in particular by +:ref:`reserving notations `. + +Parsing +~~~~~~~ + +During :gdef:`parsing` the sequence of tokens is interpreted as a +tree, for instance here: + +.. code-block:: text + :name: after-parsing + + Check + | + + + / \ + 1 * + / \ + 2 2 + +The parsed grammar can be modified, for instance by +:ref:`reserving notations `. + +Synterp +~~~~~~~ + +In addition to the above lexing and parsing, the :gdef:`synterp` phase +does just enough to be able to parse the remaining commands. +Typically, this means applying the effects of :cmd:`Reserved Notation` +commands. Plugins loading, :cmd:`Require` and :cmd:`Import` commands +can also have synterp effects. + +Interp +~~~~~~ + +The :gdef:`interp` phase performs the specific effect of each command. +If the command contains terms, they will be processed in distinct +steps as explained below. + +.. note:: + + Depending on the Rocq interface used (``rocq compile``, ``rocq + top`` or various IDEs), Rocq may run the interp phase for each + command immediately after its synterp phase, or it may run the + synterp phase for every command in the file before running any + interp step, or any other interleaving. + +===================== +Term level processing +===================== + +It is in theory possible to write down every term explicitly +as described in the :ref:`Core Language ` part of this +manual, for instance +:n:`Nat.add (S O) (Nat.mul (S (S O)) (S (S O)))`. However, this would +be very tedious and error-prone and takes us away from our usual +mathematical practice. To circumvent this, Rocq offers multiple +preprocessing mechanisms to help fill the gap between what the users +would like to input to the system and the fully formal core language +expected by the kernel. We give an overview of all these steps below. + +For instance, the notation mechanisms reflect the eponymous mathematical +practice and allows to write :n:`1 + 2 * 2` instead of the above +term. Those mechanisms range from simple :ref:`Abbreviations` to full +fledged :ref:`Notations` with user defined :ref:`syntaxes +`. Multiple interpretations can be given to the +same syntax in different contexts thanks to the :ref:`scope +` mechanism. For instance :n:`(1 + 2 * 2)%N` can be +the above natural number expression while :n:`(1 + 2 * 2)%Z` can be +an expression with integers. + +In order to take the best part of all these preprocessing mechanisms, +one needs a basic understanding of the multiple steps needed to +transform an inputted term (possibly with notations) into the valid +Gallina term which Rocq will ultimately use internally. Terms given as input +to Rocq go through several successive steps: + +* First, :term:`lexing`, then :term:`parsing`, are performed as part + of any command processing, as described above. + +* During :gdef:`internalization` a number of things are resolved. This + includes :ref:`name resolution `, :term:`notation + interpretation` and introduction of :term:`holes ` for :ref:`implicit + arguments `. + :gdef:`Notation interpretation ` + translates each syntactic element to a term, + for instance :n:`1` can be interpreted as the + natural number :n:`S O` then :n:`2` is interpreted as :n:`S (S O)`, + then :n:`2 * 2` as :n:`Nat.mul (S (S O)) (S (S O))` and finally our + whole term as :n:`Nat.add (S O) (Nat.mul (S (S O)) (S (S O)))`. The + same expression can be given multiple interpretations in various + contexts thanks to :ref:`Scopes`. + +* Finally, :gdef:`type inference`, can use the various mechanisms described in + this section to fill gaps (for instance with :ref:`canonical structures + ` or :ref:`typeclasses`) or fix terms (for + instance with :ref:`coercions `) to obtain fully detailed terms in + the :ref:`Core Language `. + +For each term, Rocq performs these steps *successively* and +*independently*. +Then, the result goes through the type checking phases discussed in +:ref:`previous chapter `. +None of the steps has any impact on the previous ones. +In particular, no typechecking is involved during parsing or +internalization. Also note that none of the features resolved during +these phases, like unqualified names, implicit arguments or notations, +remains during the later type inference and type checking phases. + +.. note:: + + The :term:`type inference` phase together with, all or part of, the + previous steps is sometimes called elaboration in the literature. + +.. example:: Simple interleaving of intern and type inference phases + + The command :g:`Definition foo : T := body.` has a trivial + :term:`synterp` phase. Indeed, it doesn't influence any further + parsing. Its :term:`interp` phase will internalize :g:`T` and infer + types in it, then it will internalize :g:`body` and infer types in + it, using :g:`T` as expected type. Note that the result of type + inference in :g:`T` matters in internalization of :g:`body`, for + instance for selecting notation scopes. Finally, the resulting + :g:`foo : T := body` is sent to the kernel. + +.. example:: Delayed steps + + :g:`Ltac foo := exact term.` will internalize :g:`term` and save + the result. Only when the :g:`foo` tactic will be called, will the + type inference on the resulting :n:`term` be run, with the type of + the current goal as expected type. If this succeeds, the proof + state will be updated to fill the goal, and the kernel will see the + result at :cmd:`Qed`. + +.. example:: Reserved notation + + The command :g:`Reserved Notation "x + y" (at level 50, left + associativity).` has a non trivial synterp phase, as it extends the + parser so that :n:`_ + _` can later be parsed. Its interp phase is + then trivial, as there is nothing left to do. diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst index bdde1da22320..7b0f0e8d89c4 100644 --- a/doc/sphinx/language/extensions/index.rst +++ b/doc/sphinx/language/extensions/index.rst @@ -4,7 +4,7 @@ Language extensions =================== -Elaboration extends the language accepted by the Rocq kernel to make it +Syntax extensions and :term:`type inference` extend the language accepted by the Rocq kernel to make it easier to use. For example, this lets the user omit most type annotations because they can be inferred, call functions with implicit arguments which will be inferred as well, extend the syntax with @@ -16,6 +16,7 @@ language presented in the :ref:`previous chapter `. .. toctree:: :maxdepth: 1 + compil-steps evars implicit-arguments match diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 311d78c81b4c..6d6a724686d9 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -823,6 +823,14 @@ Similarly variables of type `preterm` have an antiquotation It is equivalent to pretyping the preterm with the appropriate typing constraint. +Variables of type `ident` have an antiquotation + +.. prodn:: term += $preterm:@lident + +interpreting the ident as an hypothesis. This is for dynamically-named +hypotheses where `&` is for statically-named hypotheses, in other +words `let x := @y in constr:($hyp:x)` is equivalent to `constr:(&y)`. + Variables of type `pattern` have an antiquotation .. prodn:: term += $pattern:@lident diff --git a/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst b/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst index 5f070dd582dd..5de1a2dc6ec2 100644 --- a/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst +++ b/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst @@ -367,11 +367,13 @@ Induction .. example:: :n:`induction` with :n:`@occurrences` + `induction in` is useful to generalize over other variables: + .. rocqtop:: reset all - Lemma induction_test2 : forall n:nat, n = n -> n <= n. - intros. - induction n in H |-. + Lemma induction_test2 : forall n m:nat, n = m -> n <= m. + intros n m H. + induction n in m, H |- *. Show 2. .. tacn:: einduction {+, @induction_clause } {? @induction_principle } diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 92e6d242e5ef..1a895fd98a5c 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -228,7 +228,7 @@ interfere with one another, making some of them unusable. For instance, a notati and ``y`` at level 69 would be broken by another rule that puts ``y`` at another level, like ``x << y << z`` with ``x`` at level 69 and ``y`` at level 200. To avoid such issues, you should left factorize rules, that is ensure -that common prefixes use the samel levels. +that common prefixes use the same levels. .. rocqtop:: all @@ -1024,11 +1024,6 @@ the next command fails because p does not bind in the instance of n. Fail Check (exists_different p). -.. rocqtop:: in - - Notation "[> a , .. , b <]" := - (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). - Notations with expressions used both as binder and term +++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1051,7 +1046,7 @@ variant: .. rocqtop:: in reset Definition force2 q (P:nat*nat -> Prop) := - (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). + (forall n', n' >= fst q -> forall p', p' >= snd q -> P (n', p')). Notation "▢_ p P" := (force2 p (fun p => P)) (at level 0, p pattern at level 0, P at level 9, format "▢_ p P"). @@ -1337,7 +1332,7 @@ associated with the custom entry ``expr``. The level can be omitted, as in in which case Rocq infer it. If the sub-expression is at a border of the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is determined by the associativity. If the sub-expression is not at the -border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is +border of the notation (as e.g. ``e`` in ``"[ e ]"``), the level is inferred to be the highest level used for the entry. In particular, this level depends on the highest level existing in the entry at the time of use of the notation. @@ -1984,7 +1979,7 @@ Abbreviations .. rocqtop:: in reset Definition force2 q (P:nat*nat -> Prop) := - (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). + (forall n', n' >= fst q -> forall p', p' >= snd q -> P (n', p')). Notation F p P := (force2 p (fun p => P)). Check exists x y, F (x,y) (x >= 1 /\ y >= 2). diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 916c5e09191a..8858da6abe2b 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -623,12 +623,6 @@ constructors_or_record: [ | DELETENT ] -(* decl_notations not allowed for Record, Structure or Class *) -record_field: [ -| REPLACE quoted_attributes record_binder OPT [ "|" natural ] decl_notations -| WITH quoted_attributes record_binder OPT [ "|" natural ] -] - record_fields: [ | REPLACE record_field ";" record_fields | WITH OPT [ LIST1 record_field SEP ";" OPT ";" ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 92c947cf6f62..b3cc50e34a02 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -533,7 +533,7 @@ record_definition: [ ] record_field: [ -| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] name OPT field_spec OPT [ "|" natural ] +| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] name OPT field_spec OPT [ "|" natural ] OPT decl_notations ] field_spec: [ diff --git a/dune b/dune index 890389fe214e..6443ad161ecd 100644 --- a/dune +++ b/dune @@ -2,6 +2,9 @@ (env (dev (flags :standard -w -9-27@60-69@70 \ -short-paths) (coq (flags :standard -w +default))) + (br_timing + (flags :standard) + (ocamlopt_flags :standard -O3 -unbox-closures)) (release (flags :standard) (ocamlopt_flags :standard -O3 -unbox-closures)) (ireport (flags :standard -w -9-27+60-70) @@ -78,10 +81,10 @@ (run tools/dune_rule_gen/gen_rules.exe Ltac2 theories/Ltac2 -noinit -split %{env:COQ_DUNE_EXTRA_OPT=})))) ; Use summary.log as the target -(alias - (name runtest) - (package rocq-test-suite) - (deps test-suite/summary.log)) +; (alias +; (name runtest) +; (package rocq-test-suite) +; (deps test-suite/summary.log)) ; For make compat (alias diff --git a/dune-project b/dune-project index 2a6c34dddd75..3efdbbbc682b 100644 --- a/dune-project +++ b/dune-project @@ -13,7 +13,7 @@ (generate_opam_files true) (license LGPL-2.1-only) -(maintainers "The Rocq development team ") +(maintainers "The Rocq development team ") (authors "The Rocq development team, INRIA, CNRS, and contributors") ; This generates bug-reports and dev-repo (source (github rocq-prover/rocq)) @@ -57,8 +57,8 @@ prelude, now living in the rocq-core package.")) (name rocq-devtools) (depends (rocq-runtime (= :version)) - yojson - camlzip) + (yojson (>= 2.0)) + camlzip) (synopsis "Development tools for Rocq") (description "The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable @@ -128,26 +128,9 @@ implementation of Rocq's [XML protocol](https://github.com/rocq-prover/rocq/blob which allows clients, such as RocqIDE, to interact with the Rocq Prover in a structured way.")) -(package - (name rocqide) - (depends - (ocamlfind :build) - (conf-findutils :build) - conf-adwaita-icon-theme - (coqide-server (= :version)) - (cairo2 (>= 0.6.4)) - (lablgtk3-sourceview3 (and (>= 3.1.2) (or (>= 3.1.5) (<> :os "windows"))))) - (synopsis "The Rocq Prover --- GTK3 IDE") - (description "The Rocq Prover is an interactive theorem prover, or proof assistant. It provides -a formal language to write mathematical definitions, executable -algorithms and theorems together with an environment for -semi-interactive development of machine-checked proofs. - -This package provides the RocqIDE, a graphical user interface for the -development of interactive proofs.")) - (package (name rocq-test-suite) + (allow_empty) (depends (rocq-core (= :version)) coqide-server diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 23a8c9526e58..20fec16547d4 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -349,6 +349,11 @@ let csubst_instance subst ctx = in List.fold_right fold ctx SList.empty +let ext_rev_subst (subst, _, _) id0 = + match Id.Map.find id0 subst.csubst_rev with + | SRel n -> EConstr.mkRel (subst.csubst_len - n) + | SVar id -> EConstr.mkVar id + let default_ext_instance (subst, _, ctx) = csubst_instance subst (named_context_of_val ctx) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 8457c2c428a8..7825e2576f5b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -237,6 +237,8 @@ type ext_named_context = val default_ext_instance : ext_named_context -> constr SList.t +val ext_rev_subst : ext_named_context -> Id.t -> constr + val push_rel_decl_to_named_context : hypnaming:naming_mode -> evar_map -> rel_declaration -> ext_named_context -> ext_named_context diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 1b7f2799e241..bcaac2194299 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -182,9 +182,23 @@ struct [split] is pattern-matching. *) type ('a, 'i, 'o, 'e) t = - { iolist : 'r. 'i -> ('e -> 'r NonLogical.t) -> - ('a -> 'o -> ('e -> 'r NonLogical.t) -> 'r NonLogical.t) -> - 'r NonLogical.t } + { iolist : 'r. 'i -> ('e -> 'r) -> ('a -> 'o -> ('e -> 'r) -> 'r) -> 'r } + (* IMPORTANT: to play well with side-effects, all functions involved in the + above type must have AT LEAST the same arity as the one implied by their + type. This is to ensure that applying them to the expected arguments only + triggers side-effects once fully applied. If OCaml had a type for pure + functions a ~> b ⊆ a -> b, we could write this type instead as + + type ('a, 'i, 'o, 'e) t = + { iolist : 'r. 'i ~> ('e -> 'r) ~> ('a ~> 'o ~> ('e -> 'r) -> 'r) -> 'r } + + Alternatively we could use records but then it would incur a runtime + overhead. + + An easy way to ensure that is to eta-expand the functions on sight. + + Since the type is abstract in the API, this means we must locally enforce + this property only in this module. *) let return x = { iolist = fun s nil cons -> cons x s nil } @@ -210,7 +224,7 @@ struct { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) } let lift m = - { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) } + { iolist = fun s nil cons -> cons (m ()) s nil } (** State related *) @@ -243,35 +257,34 @@ struct (** For [reflect] and [split] see the "Backtracking, Interleaving, and Terminating Monad Transformers" paper. *) - type ('a, 'e) reified = ('a, ('a, 'e) reified_, 'e) list_view_ NonLogical.t + type ('a, 'e) reified = ('a, ('a, 'e) reified_, 'e) list_view_ and ('a, 'e) reified_ = {r : 'e -> ('a, 'e) reified} [@@unboxed] - let rec reflect (m : ('a * 'o, 'e) reified) = - { iolist = fun s0 nil cons -> - let next = function + let rec reflect0 : type r. _ -> _ -> _ -> (_ -> r) -> (_ -> _ -> (_ -> r) -> r) -> r = + fun e m s0 nil cons -> + match m e with | Nil e -> nil e - | Cons ((x, s), {r=l}) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons) - in - NonLogical.(m >>= next) - } + | Cons ((x, s), {r=l}) -> cons x s (fun e -> reflect0 e l s0 nil cons) + + let reflect (e : 'e) (m : 'e -> ('a * 'o, 'e) reified) = + { iolist = fun s0 nil cons -> reflect0 e m s0 nil cons } let split m : (_ list_view, _, _, _) t = - let rnil e = NonLogical.return (Nil e) in - let rcons p s l = NonLogical.return (Cons ((p, s), {r=l})) in + let rnil e = Nil e in + let rcons p s l = Cons ((p, s), {r=l}) in { iolist = fun s nil cons -> - let open NonLogical in - m.iolist s rnil rcons >>= begin function + begin match m.iolist s rnil rcons with | Nil e -> cons (Nil e) s nil | Cons ((x, s), {r=l}) -> - let l e = reflect (l e) in + let l e = reflect e l in cons (Cons (x, l)) s nil end } let run m s = - let rnil e = NonLogical.return (Nil e) in + let rnil e = Nil e in let rcons x s l = let p = (x, s) in - NonLogical.return (Cons (p, {r=l})) + Cons (p, {r=l}) in m.iolist s rnil rcons @@ -380,10 +393,10 @@ struct let run m r s = let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in - let rnil e = NonLogical.return (Nil e) in + let rnil e = Nil e in let rcons x s l = let p = (x, s.sstate, s.wstate, s.ustate) in - NonLogical.return (Cons (p, {r=l})) + Cons (p, {r=l}) in m.iolist s rnil rcons diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 91e6d3e22d88..0f72c2422651 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -148,7 +148,7 @@ module BackState : sig type ('a, 'e) reified type ('a, 'e) reified_ - val repr : ('a, 'e) reified -> ('a, ('a, 'e) reified_, 'e) list_view_ NonLogical.t + val repr : ('a, 'e) reified -> ('a, ('a, 'e) reified_, 'e) list_view_ val run : ('a, 'i, 'o, 'e) t -> 'i -> ('a * 'o, 'e) reified @@ -204,7 +204,7 @@ module Logical (P:Param) : sig type 'a reified = ('a, Exninfo.iexn) BackState.reified type 'a reified_ = ('a, Exninfo.iexn) BackState.reified_ - val repr : 'a reified -> ('a, 'a reified_, Exninfo.iexn) list_view_ NonLogical.t + val repr : 'a reified -> ('a, 'a reified_, Exninfo.iexn) list_view_ val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified diff --git a/engine/proofview.ml b/engine/proofview.ml index 164f3a70b648..e95bd32e6374 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -247,7 +247,6 @@ let apply ~name ~poly env t sp = let open Logic_monad in NewProfile.profile "Proofview.apply" (fun () -> let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in - let ans = Logic_monad.NonLogical.run ans in match ans with | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info) | Cons ((r, (state, env), status, info), _) -> @@ -1032,7 +1031,7 @@ let tclTIMEOUTF n t = Proof.current >>= fun envvar -> Proof.lift begin let open Logic_monad.NonLogical in - timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r -> + timeout n (make (fun () -> Proof.repr (Proof.run t envvar initial))) >>= fun r -> match r with | None -> return (Util.Inr (Logic_monad.Tac_Timeout, Exninfo.null)) | Some (Logic_monad.Nil e) -> return (Util.Inr e) diff --git a/engine/uState.ml b/engine/uState.ml index 875255adb8b1..11e66d0cb15e 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -78,7 +78,7 @@ let rec repr q m = match QMap.find q m.qmap with let is_above_prop q m = QSet.mem q m.above -let is_rigid m q = QSet.mem q m.rigid +let is_rigid m q = QSet.mem q m.rigid || not (QMap.mem q m.qmap) let set q qv m = let q = repr q m in diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 060d5d569821..2bee660b00f7 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -57,7 +57,7 @@ let constraint_add_leq v u c = else if j <= -1 (* n = m+k, v+k <= u and k>0 *) then if Level.equal x y then (* u+k <= u with k>0 *) Constraints.add (x,Lt,x) c - else CErrors.anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.") + else CErrors.user_err (Pp.str"Unable to handle arbitrary u+k <= v constraints.") else if j = 0 then Constraints.add (x,Le,y) c else (* j >= 1 *) (* m = n + k, u <= v+k *) diff --git a/ide/rocqide/dune b/ide/rocqide/dune index f24e2c1dde44..f564e3ce5d7a 100644 --- a/ide/rocqide/dune +++ b/ide/rocqide/dune @@ -16,17 +16,6 @@ (libraries rocq-runtime.toplevel coqide-server.protocol platform_specific) (link_flags -linkall)) -; IDE Client, we may want to add the macos_prehook.ml conditionally. -(library - (name rocqide_gui) - (wrapped false) - (modules (:standard \ document idetop rocqide_main default_bindings_src gen_gtk_platform - shared shared_os_specific)) - (foreign_stubs - (language c) - (names rocqide_os_stubs)) - (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3 platform_specific)) - (library (name platform_specific) (wrapped false) @@ -61,17 +50,6 @@ (targets shared_os_stubs.c) (action (copy shared_%{read:gtk_platform.conf}.c.in %{targets}))) -(executable - (name rocqide_main) - (public_name rocqide) - (package rocqide) - (modules rocqide_main) - (modes exe byte) - (libraries rocqide_gui)) - -(documentation - (package rocqide)) - ; Input-method bindings (executable (name default_bindings_src) @@ -81,15 +59,3 @@ (targets default.bindings) (deps (:gen ./default_bindings_src.exe)) (action (run %{gen} %{targets}))) - -; FIXME: we should install those in share/rocqide. We better do this -; once the make-based system has been phased out. -(install - (section share_root) - (package rocqide) - (files - (coq.png as coq/coq.png) - (default.bindings as coq/default.bindings) - (coq_style.xml as coq/coq_style.xml) - (coq.lang as coq/coq.lang) - (coq-ssreflect.lang as coq/coq-ssreflect.lang))) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ca9710b07aa1..9fb24b7bd555 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -416,7 +416,7 @@ let rec extern_cases_pattern_in_scope ((custom,(lev_after:int option)),scopes as match extern_record_pattern cstrsp args with | Some l -> CPatRecord l | None -> - let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in + let c = extern_reference vars (GlobRef.ConstructRef cstrsp) in if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 60aca0d9d84b..75cbed0d94ba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1348,7 +1348,7 @@ let find_projection_data c = match DAst.get c with | GApp (r, l) -> begin match DAst.get r with - | GRef (GlobRef.ConstRef cst,us) -> Some (cst, us, l, Structure.projection_nparams cst - List.length l) + | GRef (GlobRef.ConstRef cst,us) -> Some (cst, us, l, Structure.projection_nparams cst) | _ -> None end | GRef (GlobRef.ConstRef cst,us) -> Some (cst, us, [], Structure.projection_nparams cst) @@ -2580,7 +2580,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = if expl then [], [] else - let ngivenparams = List.count (fun (_,x) -> Option.is_empty x) args1 in + let ngivenparams = List.length args0 + List.count (fun (_,x) -> Option.is_empty x) args1 in let nextraargs = List.length args2 in match select_impargs_size_for_proj ~nexpectedparams ~ngivenparams ~nextraargs impls with | Inl (imps1,imps2) -> (imps1,imps2) @@ -2590,7 +2590,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = user_err ?loc:qid.CAst.loc (str "Projection " ++ pr_qualid qid ++ str " expected " ++ pr_choice int l ++ str (String.plural n " explicit parameter") ++ str ".") in - let subscopes1, subscopes2 = List.chop (nexpectedparams + 1) subscopes in + let subscopes1, subscopes2 = try List.chop (nexpectedparams + 1) subscopes with Failure _ -> subscopes, [] in let c,args1 = List.sep_last (intern_impargs head env imps1 subscopes1 (args1@[c,None])) in let p = DAst.make ?loc (GProj ((p,us),args0@args1,c)) in let args2 = intern_impargs head env imps2 subscopes2 args2 in diff --git a/interp/modintern.ml b/interp/modintern.ml index b8191389a46c..5ebcfeacae1b 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -53,12 +53,12 @@ let lookup_module_or_modtype kind qid = try if kind == ModType then raise Not_found; let mp = Nametab.locate_module qid in - Dumpglob.dump_modref ?loc mp "modtype"; (mp,Module) + Dumpglob.dump_modref ?loc mp "mod"; (mp,Module) with Not_found -> try if kind == Module then raise Not_found; let mp = Nametab.locate_modtype qid in - Dumpglob.dump_modref ?loc mp "mod"; (mp,ModType) + Dumpglob.dump_modref ?loc mp "modtype"; (mp,ModType) with Not_found as exn -> let _, info = Exninfo.capture exn in error_not_a_module_loc ~info kind loc qid diff --git a/interp/notation.ml b/interp/notation.ml index 01e93a513ae8..eec924d3d7e3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -2495,8 +2495,8 @@ let error_notation_not_reference ?loc ntn ntns = let interp_notation_as_global_reference_expanded ?loc ~head test ntn sc = let scopes = match sc with | Some sc -> - let scope = find_scope (find_delimiters_scope sc) in - String.Map.add sc scope String.Map.empty + let scope = find_delimiters_scope sc in + String.Map.singleton scope (find_scope scope) | None -> !scope_map in let ntns = browse_notation true ntn scopes in let refs = List.map (global_reference_of_notation ~head test) ntns in diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index f0eb09c1ffcd..ad7c7a3503b7 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -613,16 +613,17 @@ let subst_context env ctx = let subs = comp_subs el_id env in subst_context subs ctx -let it_mkLambda_or_LetIn ctx t = +let it_mkLambda_or_LetIn infos ctx t = + let l = Range.length (info_relevances infos) in let open Context.Rel.Declaration in match List.rev ctx with | [] -> t | LocalAssum (n, ty) :: ctx -> let assums, ctx = List.map_until (function LocalAssum (n, ty) -> Some (n, ty) | LocalDef _ -> None) ctx in let assums = (n, ty) :: assums in - { term = FLambda(List.length assums, assums, Term.it_mkLambda_or_LetIn (term_of_fconstr t) (List.rev ctx), (subs_id 0, UVars.Instance.empty)); mark = t.mark } + { term = FLambda(List.length assums, assums, Term.it_mkLambda_or_LetIn (term_of_fconstr t) (List.rev ctx), (subs_id l, UVars.Instance.empty)); mark = t.mark } | LocalDef _ :: _ -> - mk_clos (subs_id 0, UVars.Instance.empty) (Term.it_mkLambda_or_LetIn (term_of_fconstr t) ctx) + mk_clos (subs_id l, UVars.Instance.empty) (Term.it_mkLambda_or_LetIn (term_of_fconstr t) ctx) (* fstrong applies unfreeze_fun recursively on the (freeze) term and * yields a term. Assumes that the unfreeze_fun never returns a @@ -1648,7 +1649,7 @@ and match_elim : 'a. ('a, 'a patstate) reduction -> _ -> _ -> pat_state:(fconstr and match_arg : 'a. ('a, 'a patstate) reduction -> _ -> _ -> pat_state:(fconstr, stack, _, 'a) depth -> _ -> _ -> _ -> _ -> _ -> 'a = fun red info tab ~pat_state next context states patterns t -> let match_deeper = ref false in - let t' = it_mkLambda_or_LetIn context t in + let t' = it_mkLambda_or_LetIn info context t in let patterns, states = Array.split @@ Array.map2 (function Dead -> fun _ -> Ignore, Dead | (Live ({ subst; _ } as psubst) as state) -> function | Ignore -> Ignore, state diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ed45d0550e16..880ed6439bee 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -996,7 +996,7 @@ let get_recargs_approx ?evars env tree ind args = build_recargs_nested (env,[]) tree (ind, args) (* [restrict_spec env spec p] restricts the size information in spec to what is - allowed to flow through a match with predicate p in environment env. *) + allowed to flow out of a match with predicate p in environment env. *) let restrict_spec ?evars env spec p = match spec with | Not_subterm | Internally_bound_subterm _ -> spec @@ -1022,6 +1022,44 @@ let restrict_spec ?evars env spec p = end | _ -> Not_subterm +(* [filter_stack_domain env spec p] restricts the size information in stack to + what is allowed to enter under a match with predicate p in environment env. *) +let filter_stack_domain stack_element_specif set_iota_specif ?evars env p stack = + let absctx, ar = Term.decompose_lambda_decls p in + (* Optimization: if the predicate is not dependent, no restriction is needed + and we avoid building the recargs tree. *) + if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack + else let env = push_rel_context absctx env in + let rec filter_stack env ar stack = + match stack with + | [] -> [] + | elt :: stack' -> + let t = whd_all ?evars env ar in + match kind t with + | Prod (n,a,c0) -> + let d = LocalAssum (n,a) in + let ctx, a = whd_decompose_prod_decls ?evars env a in + let env = push_rel_context ctx env in + let ty, args = decompose_app_list (whd_all ?evars env a) in + let elt = match kind ty with + | Ind ind -> + let spec = stack_element_specif ?evars elt in + let sarg = + lazy (match Lazy.force spec with + | Not_subterm | Dead_code | Internally_bound_subterm _ as spec -> spec + | Subterm(l,s,path) -> + let recargs = get_recargs_approx ?evars env path ind args in + let path = inter_wf_paths path recargs in + Subterm(l,s,path)) + in + SArg sarg + | _ -> SArg (set_iota_specif (lazy Not_subterm)) + in + elt :: filter_stack (push_rel d env) c0 stack' + | _ -> List.fold_right (fun _ l -> SArg (set_iota_specif (lazy Not_subterm)) :: l) stack [] + in + filter_stack env ar stack + (* [subterm_specif renv t] computes the recursive structure of [t] and compare its size with the size of the initial recursive argument of the fixpoint we are checking. [renv] collects such information @@ -1035,17 +1073,18 @@ let rec subterm_specif ?evars renv stack t = | Rel k -> subterm_var k renv | Case (ci, u, pms, p, iv, c, lbr) -> (* iv ignored: it's just a cache *) let (ci, (p,_), _iv, c, lbr) = expand_case renv.env (ci, u, pms, p, iv, c, lbr) in - let stack' = push_stack_closures renv l stack in - let cases_spec = - branches_specif renv (lazy_subterm_specif ?evars renv [] c) ci - in - let stl = - Array.mapi (fun i br' -> - let stack_br = push_stack_args (cases_spec.(i)) stack' in - subterm_specif ?evars renv stack_br br') - lbr in - let spec = subterm_spec_glb stl in - restrict_spec ?evars renv.env spec p + let stack' = push_stack_closures renv l stack in + let stack' = filter_stack_domain stack_element_specif Fun.id ?evars renv.env p stack' in + let cases_spec = + branches_specif renv (lazy_subterm_specif ?evars renv [] c) ci + in + let stl = + Array.mapi (fun i br' -> + let stack_br = push_stack_args (cases_spec.(i)) stack' in + subterm_specif ?evars renv stack_br br') + lbr in + let spec = subterm_spec_glb stl in + restrict_spec ?evars renv.env spec p | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> (* when proving that the fixpoint f(x)=e is less than n, it is enough @@ -1206,42 +1245,6 @@ let check_is_subterm x tree = | Not_subterm | Subterm (_,Large,_) -> InvalidSubterm | Internally_bound_subterm l -> NeedReduceSubterm l -let filter_stack_domain ?evars env nr p stack = - let absctx, ar = Term.decompose_lambda_decls p in - (* Optimization: if the predicate is not dependent, no restriction is needed - and we avoid building the recargs tree. *) - if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack - else let env = push_rel_context absctx env in - let rec filter_stack env ar stack = - match stack with - | [] -> [] - | elt :: stack' -> - let t = whd_all ?evars env ar in - match kind t with - | Prod (n,a,c0) -> - let d = LocalAssum (n,a) in - let ctx, a = whd_decompose_prod_decls ?evars env a in - let env = push_rel_context ctx env in - let ty, args = decompose_app_list (whd_all ?evars env a) in - let elt = match kind ty with - | Ind ind -> - let spec = stack_element_specif ?evars elt in - let sarg = - lazy (match Lazy.force spec with - | Not_subterm | Dead_code | Internally_bound_subterm _ as spec -> spec - | Subterm(l,s,path) -> - let recargs = get_recargs_approx ?evars env path ind args in - let path = inter_wf_paths path recargs in - Subterm(l,s,path)) - in - SArg sarg - | _ -> SArg (set_iota_specif nr (lazy Not_subterm)) - in - elt :: filter_stack (push_rel d env) c0 stack' - | _ -> List.fold_right (fun _ l -> SArg (set_iota_specif nr (lazy Not_subterm)) :: l) stack [] - in - filter_stack env ar stack - let find_uniform_parameters recindx nargs bodies = let nbodies = Array.length bodies in let min_indx = Array.fold_left min nargs recindx in @@ -1379,7 +1382,7 @@ let check_one_fix ?evars renv recpos trees def = let nr = redex_level rs' in let case_spec = branches_specif renv (set_iota_specif nr (lazy_subterm_specif ?evars renv [] c_0)) ci in - let stack' = filter_stack_domain ?evars renv.env nr p stack in + let stack' = filter_stack_domain stack_element_specif (set_iota_specif nr) ?evars renv.env p stack in let rs' = Array.fold_left_i (fun k rs' br' -> let stack_br = push_stack_args case_spec.(k) stack' in diff --git a/kernel/modops.ml b/kernel/modops.ml index f38c425ec9d7..f81d75cbe90d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -277,7 +277,7 @@ let rec strengthen_and_subst_module mb subst mp_from mp_to = strengthen_module_body ~src:mp_from (NoFunctor struc') reso' mb | MoreFunctor _ -> let subst = add_mp mp_from mp_to (empty_delta_resolver mp_to) subst in - subst_module subst_dom subst mp_from mb + subst_module subst_dom_codom subst mp_from mb and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = let strengthen_and_subst_field reso' item = match item with diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8fa4c38bcbc0..6472f43751fd 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -175,8 +175,7 @@ end type compiled_library = { comp_name : DirPath.t; comp_mod : module_body; - comp_univs : Univ.ContextSet.t; - comp_qualities : Sorts.QVar.Set.t; + comp_univs : Sorts.QVar.Set.t * Univ.ContextSet.t; comp_deps : library_info array; comp_flags : permanent_flags; } @@ -228,7 +227,8 @@ type safe_environment = modlabels : Label.Set.t; objlabels : Label.Set.t; univ : Univ.ContextSet.t; - qualities : Sorts.QVar.Set.t ; + (* maybe should be a qglobal set? *) + qualities : Sorts.QVar.Set.t; future_cst : (Constant_typing.typing_context * safe_environment * Nonce.t) HandleMap.t; required : required_lib DPmap.t; loads : (ModPath.t * module_body) list; @@ -1514,8 +1514,7 @@ let export ~output_native_objects senv dir = let lib = { comp_name = dir; comp_mod = mb; - comp_univs = senv.univ; - comp_qualities = senv.qualities; + comp_univs = senv.qualities, senv.univ; comp_deps = Array.of_list comp_deps; comp_flags = permanent_flags } in @@ -1531,9 +1530,10 @@ let import lib vmtab vodigest senv = ++ DirPath.print lib.comp_name ++ str")."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in - let env = Environ.push_context_set ~strict:true lib.comp_univs senv.env in + let qualities, univs = lib.comp_univs in + let env = Environ.push_quality_set qualities senv.env in + let env = Environ.push_context_set ~strict:true univs env in let env = Environ.link_vm_library vmtab env in - let env = Environ.push_quality_set lib.comp_qualities env in let env = let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in Modops.add_linked_module mp mb linkinfo env diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5f23851754fb..6ef8b1ef763f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -240,7 +240,7 @@ type compiled_library val dirpath_of_library : compiled_library -> DirPath.t val module_of_library : compiled_library -> Mod_declarations.module_body -val univs_of_library : compiled_library -> Univ.ContextSet.t +val univs_of_library : compiled_library -> Sorts.QVar.Set.t * Univ.ContextSet.t val check_flags_for_library : compiled_library -> safe_transformer0 val start_library : DirPath.t -> ModPath.t safe_transformer diff --git a/lib/system.ml b/lib/system.ml index 2eb45646d96e..c05f03ecd875 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -420,6 +420,6 @@ let fmt_instructions_result r = let get_toplevel_path top = let open Filename in let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0) - then "" else dirname Sys.argv.(0) ^ dir_sep in + then Boot.Env.rocqbin ^ dir_sep else dirname Sys.argv.(0) ^ dir_sep in let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in dir ^ top ^ exe diff --git a/man/dune b/man/dune index 3ce1ca6370b7..0121bc791837 100644 --- a/man/dune +++ b/man/dune @@ -7,8 +7,3 @@ (section man) (package coq-core) (files coqc.1 coqtop.1 coqtop.byte.1 coqchk.1 coqdep.1 coqdoc.1 coq_makefile.1 coq-tex.1 coqwc.1 coqnative.1)) - -(install - (section man) - (package rocqide) - (files rocqide.1)) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index e7e6faacafeb..4d90f68d8f28 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -117,15 +117,17 @@ let ind_iter_references do_term do_cons do_type ind = let cons_iter cp l = do_cons cp; List.iter type_iter l in let packet_iter i p = let () = do_type p.ip_typename_ref in - if lang () == Ocaml then - let inst = ind.ind_packets.(0).ip_typename_ref.inst in - (match ind.ind_equiv with + let () = if lang () == Ocaml then begin + let inst = ind.ind_packets.(0).ip_typename_ref.inst in + (match ind.ind_equiv with | Miniml.Equiv kne -> do_type { glob = (GlobRef.IndRef (MutInd.make1 kne, i)); inst }; - | _ -> ()); + | _ -> ()) + end + in Array.iteri (fun j -> cons_iter p.ip_consnames_ref.(j)) p.ip_types in - if lang () == Ocaml then record_iter_references do_term ind.ind_kind; - Array.iteri (fun i p -> packet_iter i p) ind.ind_packets + let () = if lang () == Ocaml then record_iter_references do_term ind.ind_kind in + Array.iteri (fun i p -> packet_iter i p) ind.ind_packets let decl_iter_references do_term do_cons do_type = let type_iter = type_iter_references do_type diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index c5bfd6e7b285..71f0653813b7 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -1838,24 +1838,27 @@ let () = in GlobEnv.register_constr_interp0 wit_ltac2_constr interp -let interp_constr_var_as_constr ?loc env sigma tycon id = - let ist = Tac2interp.get_env @@ GlobEnv.lfun env in - let env = GlobEnv.renamed_env env in - let c = Id.Map.find id ist.env_ist in - let c = Tac2ffi.to_constr c in - let t = Retyping.get_type_of env sigma c in - let j = { Environ.uj_val = c; uj_type = t } in +let check_judge ?loc env sigma tycon j = match tycon with | None -> j, sigma | Some ty -> let sigma = - try Evarconv.unify_leq_delay env sigma t ty + try Evarconv.unify_leq_delay env sigma j.Environ.uj_type ty with Evarconv.UnableToUnify (sigma,e) -> Pretype_errors.error_actual_type ?loc env sigma j ty e in {j with Environ.uj_type = ty}, sigma +let interp_constr_var_as_constr ?loc env sigma tycon id = + let ist = Tac2interp.get_env @@ GlobEnv.lfun env in + let env = GlobEnv.renamed_env env in + let c = Id.Map.find id ist.env_ist in + let c = Tac2ffi.to_constr c in + let t = Retyping.get_type_of env sigma c in + let j = { Environ.uj_val = c; uj_type = t } in + check_judge ?loc env sigma tycon j + let interp_preterm_var_as_constr ?loc env sigma tycon id = let open Ltac_pretype in let ist = Tac2interp.get_env @@ GlobEnv.lfun env in @@ -1877,11 +1880,34 @@ let interp_preterm_var_as_constr ?loc env sigma tycon id = let sigma, t, ty = Pretyping.understand_ltac_ty flags env sigma vars tycon term in Environ.make_judge t ty, sigma +exception NotFoundHypVar of Id.t * Id.t + +let () = CErrors.register_handler @@ function + | NotFoundHypVar (id0,id) -> + Some + Pp.(fmt "Hypothesis %t (value of ltac2 variable %t) not found." + (fun () -> quote (Id.print id)) + (fun () -> quote (Id.print id0))) + | _ -> None + +let interp_hyp_var_as_constr ?loc globenv sigma tycon id0 = + let ist = Tac2interp.get_env @@ GlobEnv.lfun globenv in + let env = GlobEnv.renamed_env globenv in + let v = Id.Map.find id0 ist.env_ist in + let id = Tac2ffi.to_ident v in + let c = try GlobEnv.lookup_renamed globenv id + with Not_found -> + Loc.raise ?loc (NotFoundHypVar (id0,id)) + in + let j = Retyping.get_judgment_of env sigma c in + check_judge ?loc env sigma tycon j + let () = let interp ?loc ~poly env sigma tycon (kind,id) = let f = match kind with | ConstrVar -> interp_constr_var_as_constr | PretermVar -> interp_preterm_var_as_constr + | HypVar -> interp_hyp_var_as_constr | PatternVar -> assert false in f ?loc env sigma tycon id @@ -1902,6 +1928,7 @@ let () = let () = match kind with | ConstrVar -> assert false (* checked at intern time *) | PretermVar -> assert false + | HypVar -> assert false | PatternVar -> () in let ist = Tac2interp.get_env ist.Ltac_pretype.ltac_genargs in @@ -1925,6 +1952,7 @@ let () = | ConstrVar -> mt() | PretermVar -> str "preterm:" | PatternVar -> str "pattern:" + | HypVar -> str "hyp:" in str "$" ++ ppkind ++ Id.print id) in Genprint.register_noval_print0 wit_ltac2_var_quotation pr_raw pr_glb diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml index 216cece34e69..4a0ec0af5387 100644 --- a/plugins/ltac2/tac2entries.ml +++ b/plugins/ltac2/tac2entries.ml @@ -72,6 +72,7 @@ let define_tacdef ((_,kn), def) = gdata_type = def.tacdef_type; gdata_mutable = def.tacdef_mutable; gdata_deprecation = def.tacdef_deprecation; + gdata_mutation_history = []; } in Tac2env.define_global kn data @@ -849,7 +850,7 @@ type redefinition = { redef_old : Id.t option; } -let perform_redefinition redef = +let perform_redefinition (prefix,redef) = let kn = redef.redef_kn in let data = Tac2env.interp_global kn in let body = match redef.redef_old with @@ -858,7 +859,13 @@ let perform_redefinition redef = (* Rebind the old value with a let-binding *) GTacLet (false, [Name id, data.Tac2env.gdata_expr], redef.redef_body) in - let data = { data with Tac2env.gdata_expr = body } in + let history = if Option.has_some redef.redef_old then data.gdata_mutation_history else [] in + let data = { + data with + gdata_expr = body; + gdata_mutation_history = prefix.Libobject.obj_mp :: history; + } + in Tac2env.define_global kn data let subst_redefinition (subst, redef) = @@ -870,7 +877,7 @@ let subst_redefinition (subst, redef) = let classify_redefinition o = Substitute let inTac2Redefinition : redefinition -> obj = - declare_object + declare_named_object_gen {(default_object "TAC2-REDEFINITION") with cache_function = perform_redefinition; open_function = simple_open perform_redefinition; @@ -1006,6 +1013,22 @@ end let print_constant ~print_def qid ?info data = let e = data.Tac2env.gdata_expr in let (_, t) = data.Tac2env.gdata_type in + let ismut = if data.gdata_mutable then spc() ++ str "(* mutable *)" else mt() in + let history = if not print_def then mt() + else match data.gdata_mutation_history with + | [] -> mt () + | mods -> + let pr_one mp = + let qid = try Nametab.shortest_qualid_of_module mp + with Not_found -> + try Nametab.shortest_qualid_of_dir (DirOpenModule mp) + with Not_found -> Nametab.shortest_qualid_of_dir (DirOpenModtype mp) + in + pr_qualid qid + in + let redef = prlist_with_sep fnl pr_one mods in + fnl () ++ str "Redefined by:" ++ fnl () ++ redef + in let name = int_name () in let def = if print_def then fnl () ++ hov 2 @@ -1017,7 +1040,7 @@ let print_constant ~print_def qid ?info data = | Some info -> fnl() ++ fnl() ++ hov 2 (str "Compiled as" ++ spc() ++ str info.Tac2env.source) in hov 0 ( - hov 2 (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype name t) ++ def ++ info + hov 2 (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype name t ++ ismut) ++ def ++ info ++ history ) let print_type ~print_def qid kn = diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml index 557f0af41965..a89d98e204f0 100644 --- a/plugins/ltac2/tac2env.ml +++ b/plugins/ltac2/tac2env.ml @@ -19,6 +19,7 @@ type global_data = { gdata_type : type_scheme; gdata_mutable : bool; gdata_deprecation : Deprecation.t option; + gdata_mutation_history : ModPath.t list; } type constructor_data = { @@ -303,6 +304,7 @@ type var_quotation_kind = | ConstrVar | PretermVar | PatternVar + | HypVar let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr" let wit_ltac2_var_quotation = Genarg.make0 "ltac2:quotation" diff --git a/plugins/ltac2/tac2env.mli b/plugins/ltac2/tac2env.mli index f56852cd458b..327101dd7100 100644 --- a/plugins/ltac2/tac2env.mli +++ b/plugins/ltac2/tac2env.mli @@ -24,6 +24,7 @@ type global_data = { gdata_type : type_scheme; gdata_mutable : bool; gdata_deprecation : Deprecation.t option; + gdata_mutation_history : ModPath.t list; } val define_global : ltac_constant -> global_data -> unit @@ -190,6 +191,7 @@ type var_quotation_kind = | ConstrVar | PretermVar | PatternVar + | HypVar val wit_ltac2_var_quotation : (lident option * lident, var_quotation_kind * Id.t, Util.Empty.t) genarg_type (** Ltac2 quotations for variables "$x" or "$kind:foo" in Gallina terms. diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index 94ad21ff5ad4..cacfb0298143 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -29,6 +29,7 @@ let t_string = rocq_type "string" let t_constr = rocq_type "constr" let t_preterm = rocq_type "preterm" let t_pattern = rocq_type "pattern" +let t_ident = rocq_type "ident" let t_bool = rocq_type "bool" let ltac2_env : Tac2typing_env.t Genintern.Store.field = @@ -2145,6 +2146,7 @@ let intern_var_quotation_gen ~ispat ist (kind, { CAst.v = id; loc }) = | "constr" -> ConstrVar | "preterm" -> PretermVar | "pattern" -> PatternVar + | "hyp" -> HypVar | _ -> CErrors.user_err ?loc:kind.loc Pp.(str "Unknown Ltac2 variable quotation kind" ++ spc() ++ Id.print kind.v) @@ -2162,6 +2164,11 @@ let intern_var_quotation_gen ~ispat ist (kind, { CAst.v = id; loc }) = if not ispat then CErrors.user_err ?loc Pp.(str "pattern quotations not supported outside tactic patterns.") else t_pattern + | HypVar -> + (* XXX allow this? *) + if ispat + then CErrors.user_err ?loc Pp.(str "hyp quotations not supported in tactic patterns.") + else t_ident in let env = match Genintern.Store.get ist.extra ltac2_env with | None -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index b4de6c5ce3c9..8b980f593fda 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -767,8 +767,35 @@ let pf_interp_ty ?(resolve_typeclasses=false) env sigma0 ist ty = (* TASSI: given (c : ty), generates (c ??? : ty[???/...]) with m evars *) exception NotEnoughProducts -let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m -= +let saturate ?(beta=false) ?(bi_types=false) env sigma c ?ty m = + let sigma, ty = match ty with + | Some ty -> sigma, ty + | None -> + if Termops.is_template_polymorphic_ref env sigma c then + begin match EConstr.kind sigma c with + | Ind (ind,_) -> + let sigma, univs = Typing.get_template_parameters env sigma ind ~refresh_all:true [||] in + let specif = Inductive.lookup_mind_specif env ind in + let typ, csts = Inductive.type_of_inductive_knowing_parameters + (specif,UVars.Instance.empty) + univs + in + let sigma = Evd.add_constraints sigma csts in + sigma, EConstr.of_constr typ + | Construct ((ind,_ as ctor),_) -> + let sigma, univs = Typing.get_template_parameters env sigma ind ~refresh_all:true [||] in + let specif = Inductive.lookup_mind_specif env ind in + let typ, csts = Inductive.type_of_constructor_knowing_parameters + (ctor,UVars.Instance.empty) + specif + univs + in + let sigma = Evd.add_constraints sigma csts in + sigma, EConstr.of_constr typ + | _ -> assert false + end + else sigma, Retyping.get_type_of env sigma c + in let rec loop ty args sigma n = let open EConstr in if n = 0 then diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index c70716898bb3..78c1f96f9a89 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -178,6 +178,16 @@ let interp_ltac_variable ?loc typing_fun env sigma id : Evd.evar_map * unsafe_ju let interp_ltac_id env id = ltac_interp_id env.lvar id +let lookup_renamed globenv id = + let env = renamed_env globenv in + (* optimization: if id is in the original named context it will + be the same in the extended context *) + match EConstr.lookup_named id env with + | d -> EConstr.mkVar id + | exception Not_found -> + let (_, _, sign) as ext = Lazy.force globenv.extra in + Evarutil.ext_rev_subst ext id + type 'a obj_interp_fun = ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint -> 'a -> unsafe_judgment * Evd.evar_map diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 32d9160c3025..17d91760d89f 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -65,6 +65,10 @@ val new_evar : t -> evar_map -> ?src:Evar_kinds.t Loc.located -> val new_type_evar : t -> evar_map -> src:Evar_kinds.t Loc.located -> evar_map * constr +(** Lookup the ident in the context that would be used for an evar in + this environment, producing a term (Var or Rel) valid in [renamed_env]. *) +val lookup_renamed : t -> Id.t -> constr + (** [hide_variable env id] tells to hide the binding of [id] in the ltac environment part of [env]. It is useful e.g. for the dual status of [y] as term and binder. This is the case diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 5618d84766f0..09f88f3d5c9d 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -25,7 +25,7 @@ open Context.Rel.Declaration module GR = Names.GlobRef -let fresh_template_context env0 sigma ind (mib, _ as spec) args = +let fresh_template_context env0 sigma ind (mib, _ as spec) ?(refresh_all=false) args = let templ = match mib.Declarations.mind_template with | None -> assert false | Some t -> Array.of_list t.template_param_arguments @@ -42,6 +42,7 @@ let fresh_template_context env0 sigma ind (mib, _ as spec) args = if i < Array.length args then match Reductionops.sort_of_arity env sigma args.(i).uj_type with | s -> sigma, s | exception Reduction.NotArity -> Evd.new_sort_variable Evd.univ_flexible sigma + else if refresh_all then Evd.new_sort_variable Evd.univ_flexible sigma else sigma, s0 in let t = EConstr.it_mkProd_or_LetIn (mkSort s) decls in @@ -68,9 +69,9 @@ let fresh_template_context env0 sigma ind (mib, _ as spec) args = in freshen 0 env0 sigma [] [] ctx -let get_template_parameters env sigma ind args = +let get_template_parameters env sigma ind ?refresh_all args = let spec = Inductive.lookup_mind_specif env ind in - fresh_template_context env sigma ind spec args + fresh_template_context env sigma ind spec ?refresh_all args let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with diff --git a/pretyping/typing.mli b/pretyping/typing.mli index fa689ee4b4c1..81c386ae5118 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -76,4 +76,4 @@ val bad_relevance_msg : (Environ.env * evar_map * (constr, types, ERelevance.t) (** Template typing *) -val get_template_parameters : env -> evar_map -> inductive -> unsafe_judgment array -> evar_map * Inductive.param_univs +val get_template_parameters : env -> evar_map -> inductive -> ?refresh_all:bool -> unsafe_judgment array -> evar_map * Inductive.param_univs diff --git a/rocq-core.opam b/rocq-core.opam index aca5d423102d..7159280544e6 100644 --- a/rocq-core.opam +++ b/rocq-core.opam @@ -17,7 +17,9 @@ Feit-Thompson theorem or homotopy type theory) and teaching. This package includes the Rocq prelude, that is loaded automatically by Rocq in every .v file, as well as other modules bound to the Corelib.* and Ltac2.* namespaces.""" -maintainer: ["The Rocq development team "] +maintainer: [ + "The Rocq development team " +] authors: ["The Rocq development team, INRIA, CNRS, and contributors"] license: "LGPL-2.1-only" homepage: "https://rocq-prover.org/" diff --git a/rocq-devtools.opam b/rocq-devtools.opam index 0be6b82fcc0d..d1b8d7a5cd27 100644 --- a/rocq-devtools.opam +++ b/rocq-devtools.opam @@ -16,7 +16,9 @@ Feit-Thompson theorem or homotopy type theory) and teaching. This package includes tools to help when developing Rocq projects (timelog2html).""" -maintainer: ["The Rocq development team "] +maintainer: [ + "The Rocq development team " +] authors: ["The Rocq development team, INRIA, CNRS, and contributors"] license: "LGPL-2.1-only" homepage: "https://rocq-prover.org/" @@ -25,7 +27,7 @@ bug-reports: "https://github.com/rocq-prover/rocq/issues" depends: [ "dune" {>= "3.8"} "rocq-runtime" {= version} - "yojson" + "yojson" {>= "2.0"} "camlzip" "odoc" {with-doc} ] diff --git a/rocq-runtime.opam b/rocq-runtime.opam index d350be9093b4..2e22f0f5565c 100644 --- a/rocq-runtime.opam +++ b/rocq-runtime.opam @@ -20,7 +20,9 @@ not the vernacular standard library. Note that in this setup, Rocq needs to be started with the -boot and -noinit options, as will otherwise fail to find the regular Rocq prelude, now living in the rocq-core package.""" -maintainer: ["The Rocq development team "] +maintainer: [ + "The Rocq development team " +] authors: ["The Rocq development team, INRIA, CNRS, and contributors"] license: "LGPL-2.1-only" homepage: "https://rocq-prover.org/" diff --git a/rocq-test-suite.opam b/rocq-test-suite.opam index bf77496517c5..5e7e24c3c250 100644 --- a/rocq-test-suite.opam +++ b/rocq-test-suite.opam @@ -15,7 +15,9 @@ formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching. This package runs the test suite.""" -maintainer: ["The Rocq development team "] +maintainer: [ + "The Rocq development team " +] authors: ["The Rocq development team, INRIA, CNRS, and contributors"] license: "LGPL-2.1-only" homepage: "https://rocq-prover.org/" diff --git a/rocqide.opam b/rocqide.opam deleted file mode 100644 index 9fe4a6ca74c1..000000000000 --- a/rocqide.opam +++ /dev/null @@ -1,43 +0,0 @@ -# This file is generated by dune, edit dune-project instead -opam-version: "2.0" -version: "dev" -synopsis: "The Rocq Prover --- GTK3 IDE" -description: """ -The Rocq Prover is an interactive theorem prover, or proof assistant. It provides -a formal language to write mathematical definitions, executable -algorithms and theorems together with an environment for -semi-interactive development of machine-checked proofs. - -This package provides the RocqIDE, a graphical user interface for the -development of interactive proofs.""" -maintainer: ["The Rocq development team "] -authors: ["The Rocq development team, INRIA, CNRS, and contributors"] -license: "LGPL-2.1-only" -homepage: "https://rocq-prover.org/" -doc: "https://rocq-prover.org/docs/" -bug-reports: "https://github.com/rocq-prover/rocq/issues" -depends: [ - "dune" {>= "3.8"} - "ocamlfind" {build} - "conf-findutils" {build} - "conf-adwaita-icon-theme" - "coqide-server" {= version} - "cairo2" {>= "0.6.4"} - "lablgtk3-sourceview3" {>= "3.1.2" & (>= "3.1.5" | os != "windows")} - "odoc" {with-doc} -] -build: [ - ["dune" "subst"] {dev} - [ - "dune" - "build" - "-p" - name - "-j" - jobs - "@install" - "@runtest" {with-test} - "@doc" {with-doc} - ] -] -dev-repo: "git+https://github.com/rocq-prover/rocq.git" diff --git a/tactics/hints.ml b/tactics/hints.ml index 2ea831e772e3..91ac91b413da 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1622,9 +1622,18 @@ let make_local_hint_db env sigma ?ts eapply lems = make_local_hint_db env sigma ts eapply lems let make_db_list dbnames = - let use_core = not (List.mem "nocore" dbnames) in - let dbnames = List.remove String.equal "nocore" dbnames in - let dbnames = if use_core then "core"::dbnames else dbnames in + let fold (core, nocore) db = + if String.equal db "core" then (true, nocore) + else if String.equal db "nocore" then (core, true) + else (core, nocore) + in + let has_core, has_nocore = List.fold_left fold (false, false) dbnames in + let dbnames = match has_core, has_nocore with + | true, true -> user_err Pp.(str "The core and nocore databases are mutually exclusive") + | true, false -> dbnames + | false, true -> List.remove String.equal "nocore" dbnames + | false, false -> "core" :: dbnames + in let lookup db = try searchtable_map db with Not_found -> error_no_such_hint_database db in diff --git a/test-suite/bugs/bug_15815.v b/test-suite/bugs/bug_15815.v new file mode 100644 index 000000000000..0a22bc6db963 --- /dev/null +++ b/test-suite/bugs/bug_15815.v @@ -0,0 +1,11 @@ +(* Was failing with anomaly List.chop in 8.15 and was running for very long in 9.0 *) +(* This tests abbreviations with more projection parameters than allowed *) +Class my_class := { + my_class_car : Type; + my_class_field_aux : my_class_car -> nat +}. + +Notation my_class_field := (@my_class_field_aux _). + +Fail Timeout 10 Definition my_test {MC : my_class} (x : my_class_car) : nat := + x.(my_class_field). diff --git a/test-suite/bugs/bug_20582.v b/test-suite/bugs/bug_20582.v new file mode 100644 index 000000000000..58c0ada8fd07 --- /dev/null +++ b/test-suite/bugs/bug_20582.v @@ -0,0 +1,19 @@ +Require Import ssreflect. + +Section Injections. + +Variables (rT aT : Type) (f : aT -> rT). + +Definition cancel g := forall x, g (f x) = x. + +Definition pcancel g := forall x, g (f x) = Some x. + +Succeed Constraint eq.u0 < Injections.u1. + +Lemma can_pcan g : cancel g -> pcancel (fun y => Some (g y)). +Proof. by move=> fK x; congr (Some _). Defined. + +Succeed Constraint eq.u0 < Injections.u1. +Succeed Constraint Injections.u1 < eq.u0. + +End Injections. diff --git a/test-suite/bugs/bug_20728.v b/test-suite/bugs/bug_20728.v new file mode 100644 index 000000000000..3d8fcade9d53 --- /dev/null +++ b/test-suite/bugs/bug_20728.v @@ -0,0 +1,15 @@ +(* -*- mode: coq; coq-prog-args: ("-allow-rewrite-rules") -*- *) + +Inductive STrue : SProp := SI. +Inductive Box (A : SProp) : A -> Set := box a : Box A a. + +Symbol S: bool -> Type -> Set. + +Rewrite Rule S_rew := + S _ (forall (a : ?A), Box STrue ?b) => Box _ (fun a => ?b). + +Check fun (x : STrue) => + (eq_refl : S true (unit -> Box STrue x) = S false (unit -> Box STrue x)). + +Definition error (x : STrue) := + (eq_refl : S true (unit -> Box STrue x) = S false (unit -> Box STrue x)). diff --git a/test-suite/bugs/bug_20914.v b/test-suite/bugs/bug_20914.v new file mode 100644 index 000000000000..07f1fedae36c --- /dev/null +++ b/test-suite/bugs/bug_20914.v @@ -0,0 +1,6 @@ +Sort s. + +Polymorphic Definition foo@{s;u} (A:Type@{s;u}) (a:A) := a. + +(* slightly eta expanded so "s" appears in a sort and in the instance *) +Definition bla A := foo@{s;Set} A. diff --git a/test-suite/bugs/bug_20940.v b/test-suite/bugs/bug_20940.v new file mode 100644 index 000000000000..04fb8dbe7e46 --- /dev/null +++ b/test-suite/bugs/bug_20940.v @@ -0,0 +1,4 @@ +(* Was an anomaly List.chop in the presence of projections with not enough argument scopes *) +Record R (n:nat) (p: unit) (q : unit) := { field : unit }. +Arguments field n%_nat {p} {q}. +Check fun C => C.(field _). diff --git a/test-suite/bugs/bug_21051.v b/test-suite/bugs/bug_21051.v new file mode 100644 index 000000000000..7944e856033c --- /dev/null +++ b/test-suite/bugs/bug_21051.v @@ -0,0 +1,55 @@ +Module Type T. +Parameter n : bool. +End T. + +Module M. +Definition n := true. +End M. + +Module M'. +Definition n := false. +End M'. + +Module MAKE. + +Module FUN (E : T). + +Module F. +Definition bug := E.n. +End F. + +Module G := F. + +End FUN. + +End MAKE. + +Include MAKE. + +Module RES := FUN M. +Module RES' := FUN M'. + +Lemma foo : RES.G.bug = RES'.G.bug. +Proof. +Fail reflexivity. (* Was succeeding, allowing to derive False with the code below. *) +Abort. + +(* +Lemma foo0 : RES.G.bug = true. +Proof. +reflexivity. +Qed. + +Lemma foo1 : RES'.G.bug = false. +Proof. +reflexivity. +Qed. + +Lemma unsound : False. +Proof. +assert (true = false); [|congruence]. +rewrite <- foo0; rewrite <- foo1; apply foo. +Qed. + +Print Assumptions unsound. +*) diff --git a/test-suite/bugs/bug_21053.v b/test-suite/bugs/bug_21053.v new file mode 100644 index 000000000000..8d86fedc488e --- /dev/null +++ b/test-suite/bugs/bug_21053.v @@ -0,0 +1,41 @@ +Notation "'rew' [ f ] e 'in' x" := (eq_rect _ f x _ e) (at level 10, x at level 10). + +Definition cast_rev e : nat -> nat := + rew [fun (T : Set) => T -> nat] eq_sym e in fun x => x. + +Fail Fixpoint f (e : nat = nat) (n : nat) {struct n} := + match n with + | 0 => 0 + | S n => S (f e (cast_rev e n)) +end. +(* Problematic fixpoint : [cast_rev_e n] should not be a subterm of [n] *) + +#[bypass_check(guard)] +Fixpoint f (e : nat = nat) (n : nat) {struct n} := + match n with + | 0 => 0 + | S n => S (f e (cast_rev e n)) +end. + +Section Issue. +Context (e : nat = nat). (* Supposed non-trivial *) +Context (e0 : rew [fun (T : Set) => T] e in 0 = 1). +(* How the non triviality may appear *) + +Corollary e0' : cast_rev e 0 = 1. +Proof. + rewrite <- e0. clear e0. + unfold cast_rev. + generalize 0. + destruct e. + reflexivity. +Defined. + +Theorem Boom : False. + enough (f e 1 = S (f e 1)) by now induction (f e 1); auto. + change (f e 1) with (S (f e (cast_rev e 0))) at 1. + f_equal. f_equal. + apply e0'. +Qed. + +End Issue. diff --git a/test-suite/dune b/test-suite/dune.disabled similarity index 100% rename from test-suite/dune rename to test-suite/dune.disabled diff --git a/test-suite/ltac2/compat_tactics.v b/test-suite/ltac2/compat_tactics.v new file mode 100644 index 000000000000..330909b2cf20 --- /dev/null +++ b/test-suite/ltac2/compat_tactics.v @@ -0,0 +1,9 @@ +From Ltac2 Require Import Ltac2 Ltac1CompatNotations. + +(* rename *) +Goal forall (x : nat), x = x. +Proof. + intro x. + rename x into y. + exact (@eq_refl _ y). +Qed. diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v index 4396976ba0cb..663e954a1a1b 100644 --- a/test-suite/ltac2/std_tactics.v +++ b/test-suite/ltac2/std_tactics.v @@ -144,14 +144,6 @@ Proof. Std.apply true false [fun () => Control.plus (fun () => 'I) (fun _ => '0), Std.NoBindings] None. Qed. -(* rename *) -Goal forall (x : nat), x = x. -Proof. - intro x. - rename x into y. - exact (@eq_refl _ y). -Qed. - (* eassumption *) Goal forall (x : nat) y z, x = y -> y = z -> x = z. Proof. diff --git a/test-suite/output/DebugRelevances.out b/test-suite/output/DebugRelevances.out index aa2fb204efbe..d1f165479299 100644 --- a/test-suite/output/DebugRelevances.out +++ b/test-suite/output/DebugRelevances.out @@ -14,13 +14,17 @@ fun (A : (* Relevant *) SProp) (a : (* Irrelevant *) A) => a Arguments bar A%_type_scope a baz@{s ; u} = -fun (A : (* Relevant *) Type) (a : (* s *) A) => a - : forall A : (* Relevant *) Type, A -> A +fun (A : (* Relevant *) Type@{s ; _}) (a : (* s *) A) => a + : forall A : (* Relevant *) Type@{s ; _}, A -> A Arguments baz A%_type_scope a boz@{s s' ; u} = -fun (A B : (* Relevant *) Type) (a : (* s *) hide) (_ : (* s' *) hide) => a - : forall A B : (* Relevant *) Type, hide -> hide -> hide +fun (A : (* Relevant *) Type@{s ; _}) (B : (* Relevant *) Type@{s' ; _}) + (a : (* s *) hide) (_ : (* s' *) hide) => +a + : forall (A : (* Relevant *) Type@{s ; _}) + (B : (* Relevant *) Type@{s' ; _}), + hide -> hide -> hide Arguments boz (A B)%_type_scope a b 1 goal diff --git a/test-suite/output/DeclareSort.out b/test-suite/output/DeclareSort.out index e559cab858a8..e5aaed5710a4 100644 --- a/test-suite/output/DeclareSort.out +++ b/test-suite/output/DeclareSort.out @@ -24,7 +24,7 @@ fun A : Type@{s ; _} => A : Type@{s ; _} : Type@{s ; _} -> Type@{s ; _} foo : Type@{S1 ; _} -> Type@{S2 ; _} -foo@{S2 ; } : Type -> Type +foo@{S2 ; } : Type@{S1 ; _} -> Type@{S2 ; _} foo is universe polymorphic Arguments foo _%_type_scope diff --git a/test-suite/output/FixpointNoElim.out b/test-suite/output/FixpointNoElim.out new file mode 100644 index 000000000000..766ffd1f846f --- /dev/null +++ b/test-suite/output/FixpointNoElim.out @@ -0,0 +1,10 @@ +File "./output/FixpointNoElim.v", line 4, characters 0-48: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default] +File "./output/FixpointNoElim.v", line 4, characters 0-48: +The command has indeed failed with message: +Recursive definition of bar is ill-formed. +Cannot define a fixpoint +with principal argument living in sort "Type@{α3 ; Set}" +to produce a value in sort "Set" +because "Type@{α3 ; Set}" does not eliminate to "Set". +Recursive definition is: "fun _ : foo => I". diff --git a/test-suite/output/FixpointNoElim.v b/test-suite/output/FixpointNoElim.v new file mode 100644 index 000000000000..b3eca7e8442c --- /dev/null +++ b/test-suite/output/FixpointNoElim.v @@ -0,0 +1,4 @@ +Set Universe Polymorphism. +Inductive foo@{s;} : Type@{s;Set} := XX. + +Fail Fixpoint bar@{s;} (f:foo@{s;}) : True := I. diff --git a/test-suite/output/PrintMatch.out b/test-suite/output/PrintMatch.out index 0c6e6b5ff77b..eb78c3a10e5c 100644 --- a/test-suite/output/PrintMatch.out +++ b/test-suite/output/PrintMatch.out @@ -46,3 +46,12 @@ end : forall [A : Type] [x y : A], x = y -> y = x Arguments eq_sym [A]%_type_scope [x y] _ +test = +fun (O : unit) (S : nat -> unit) (n : nat) => +match n with +| 0 => O +| Datatypes.S n0 => S n0 +end + : unit -> (nat -> unit) -> nat -> unit + +Arguments test O S%_function_scope n%_nat_scope diff --git a/test-suite/output/PrintMatch.v b/test-suite/output/PrintMatch.v index 8b2a51cc0c3c..02c853ac1b7b 100644 --- a/test-suite/output/PrintMatch.v +++ b/test-suite/output/PrintMatch.v @@ -27,3 +27,15 @@ Set Asymmetric Patterns. Print eq_sym. End Bug18163. + +Module AvoidName. + +Definition test (O : unit) (S : nat -> unit) (n : nat) := +match n with +| Datatypes.O => O +| Datatypes.S n => S n +end. + +Print test. + +End AvoidName. diff --git a/test-suite/output/bug_20711.out b/test-suite/output/bug_20711.out new file mode 100644 index 000000000000..1832114dd7ba --- /dev/null +++ b/test-suite/output/bug_20711.out @@ -0,0 +1,14 @@ +module Main where + +import qualified Prelude + +data Bool = + True + | False + +type Foo = Bool + +type Wrapper = Foo + -- singleton inductive, whose constructor was Build_Wrapper + + diff --git a/test-suite/output/bug_20711.v b/test-suite/output/bug_20711.v new file mode 100644 index 000000000000..5840d6b8070b --- /dev/null +++ b/test-suite/output/bug_20711.v @@ -0,0 +1,9 @@ +Require Extraction. + +Extraction Language Haskell. + +Definition foo := bool. + +Record Wrapper := { v1 : foo; }. + +Recursive Extraction Wrapper. diff --git a/test-suite/output/bug_20754.out b/test-suite/output/bug_20754.out new file mode 100644 index 000000000000..2fc85c8634f8 --- /dev/null +++ b/test-suite/output/bug_20754.out @@ -0,0 +1,8 @@ +Notation "x * y" := (prod x y) + +prod : Type -> Type -> Type + +prod is template universe polymorphic +Arguments prod (A B)%_type_scope +Expands to: Inductive Corelib.Init.Datatypes.prod +Declared in library Corelib.Init.Datatypes, line 248, characters 10-14 diff --git a/test-suite/output/bug_20754.v b/test-suite/output/bug_20754.v new file mode 100644 index 000000000000..f77913981f30 --- /dev/null +++ b/test-suite/output/bug_20754.v @@ -0,0 +1 @@ +About "_ * _"%type. diff --git a/test-suite/output/ltac2_hyp_var.out b/test-suite/output/ltac2_hyp_var.out new file mode 100644 index 000000000000..6a9c0ea142c4 --- /dev/null +++ b/test-suite/output/ltac2_hyp_var.out @@ -0,0 +1,22 @@ +File "./output/ltac2_hyp_var.v", line 3, characters 16-18: +The command has indeed failed with message: +Unbound value id +- : constr = constr:(fun (_ : nat) (x : bool) => eq_refl : (x, x) = (x, x)) +File "./output/ltac2_hyp_var.v", line 7, characters 33-40: +The command has indeed failed with message: +Hypothesis "x" (value of ltac2 variable "id") not found. +File "./output/ltac2_hyp_var.v", line 8, characters 49-56: +The command has indeed failed with message: +In environment +x : nat +The term "x" has type "nat" while it is expected to have type "bool". +- : constr = constr:(fun x : nat => x : nat) +- : constr = constr:(fun x0 : bool => eq_refl : (x0, x) = (x0, x)) +- : constr = constr:(x : nat) +File "./output/ltac2_hyp_var.v", line 18, characters 36-43: +The command has indeed failed with message: +In environment +x : nat +The term "x" has type "nat" while it is expected to have type "bool". +- : constr = constr:(fun (_ : nat) (_0 : bool) => eq_refl : _0 = _0) +- : constr = constr:(fun (_0 : nat) (_ : bool) => eq_refl : _0 = _0) diff --git a/test-suite/output/ltac2_hyp_var.v b/test-suite/output/ltac2_hyp_var.v new file mode 100644 index 000000000000..f8a86862db9d --- /dev/null +++ b/test-suite/output/ltac2_hyp_var.v @@ -0,0 +1,25 @@ +Require Import Ltac2.Ltac2. + +Fail Check $hyp:id. + +Ltac2 Eval let id := @x in '(fun (x:nat) (x : bool) => eq_refl : (x, &x) = (x, $hyp:id)). + +Fail Ltac2 Eval let id := @x in '$hyp:id. +Fail Ltac2 Eval let id := @x in '(fun x : nat => $hyp:id : bool). + +Ltac2 Eval let id := @x in constr:(fun x => $hyp:id : nat). + +Section S. + Variable x : nat. + + Ltac2 Eval let id := @x in '(fun x : bool => eq_refl : (x, &x) = (x, $hyp:id)). + + Ltac2 Eval let id := @x in '($hyp:id : nat). + Fail Ltac2 Eval let id := @x in '($hyp:id : bool). +End S. + +Set Mangle Names. + +Ltac2 Eval let id := @x in '(fun (x:nat) (x:bool) => eq_refl : &x = $hyp:id :> bool). + +Ltac2 Eval let id := @_1 in '(fun (x:nat) (x:bool) => eq_refl : &_1 = $hyp:id :> nat). diff --git a/theories/Corelib/dune.disabled b/theories/Corelib/dune similarity index 100% rename from theories/Corelib/dune.disabled rename to theories/Corelib/dune diff --git a/theories/Ltac2/Ltac1CompatNotations.v b/theories/Ltac2/Ltac1CompatNotations.v index c826354853da..d77518e5aa86 100644 --- a/theories/Ltac2/Ltac1CompatNotations.v +++ b/theories/Ltac2/Ltac1CompatNotations.v @@ -17,4 +17,7 @@ Require Import Ltac2.Init Ltac2.Std. -Ltac2 Notation "transitivity" c(constr) := Std.transitivity c. +Ltac2 Notation "transitivity" c(constr) : 1 := Std.transitivity c. + +Ltac2 Notation "rename" renames(list1(seq(ident, "into", ident), ",")) := + Std.rename renames. diff --git a/theories/Ltac2/Notations.v b/theories/Ltac2/Notations.v index b84da7c2fabb..28fc04d49329 100644 --- a/theories/Ltac2/Notations.v +++ b/theories/Ltac2/Notations.v @@ -508,9 +508,6 @@ Ltac2 symmetry0 cl := Ltac2 Notation "symmetry" cl(opt(clause)) := symmetry0 cl. Ltac2 Notation symmetry := symmetry. -Ltac2 Notation "rename" renames(list1(seq(ident, "into", ident), ",")) := - Std.rename renames. - Ltac2 Notation "revert" ids(list1(ident)) := Std.revert ids. Ltac2 Notation assumption := Std.assumption (). diff --git a/theories/Ltac2/dune.disabled b/theories/Ltac2/dune similarity index 100% rename from theories/Ltac2/dune.disabled rename to theories/Ltac2/dune diff --git a/tools/configure/configure.ml b/tools/configure/configure.ml index e473e136bc09..9538a67fcbca 100644 --- a/tools/configure/configure.ml +++ b/tools/configure/configure.ml @@ -22,9 +22,9 @@ open CmdArgs.Prefs let (/) = Filename.concat -let coq_version = "9.1+alpha" -let vo_magic = 90099 -let is_a_released_version = false +let coq_version = "9.1.0" +let vo_magic = 90100 +let is_a_released_version = true (** Default OCaml binaries *) diff --git a/tools/coqdep/dune b/tools/coqdep/dune index 0748c46e198d..f7cb88c1460c 100644 --- a/tools/coqdep/dune +++ b/tools/coqdep/dune @@ -2,6 +2,6 @@ (executable (name coqdep) (public_name coqdep) - (package coq-core) + (package rocq-core) (modules coqdep) (libraries coqdeplib)) diff --git a/topbin/dune b/topbin/dune index 04e73b63b885..9bb85da1801f 100644 --- a/topbin/dune +++ b/topbin/dune @@ -36,7 +36,7 @@ (executable (name coqc_bin) (public_name coqc) - (package coq-core) + (package rocq-core) (modules coqc_bin) (libraries rocqshim)) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index e6594f237998..244372fb17c9 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -541,10 +541,13 @@ let explain_ill_formed_fix_body env sigma names i = function | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in str "Recursive call to " ++ called ++ str " has not enough arguments" | FixpointOnNonEliminable (s, s') -> - str "Cannot define a fixpoint on " ++ Printer.pr_sort sigma s ++ - strbrk " on a value living in " ++ Printer.pr_sort sigma s' ++ - str ": " ++ Printer.pr_sort sigma s ++ str " does not eliminate in " ++ - Printer.pr_sort sigma s' + let pr_sort u = quote @@ Flags.with_option Constrextern.print_universes (Printer.pr_sort sigma) u in + fmt "Cannot define a fixpoint@ with principal argument living in sort %t@ \ + to produce a value in sort %t@ because %t does not eliminate to %t" + (fun () -> pr_sort s) + (fun () -> pr_sort s') + (fun () -> pr_sort s) + (fun () -> pr_sort s') let explain_ill_formed_cofix_body env sigma = function (* CoFixpoint guard errors *) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 44a1f36c6649..ec6d07b85db5 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -937,6 +937,16 @@ let loc_info gr = | None -> mt() | Some loc -> cut() ++ hov 0 (str "Declared in" ++ spc() ++ pr_loc_use_dp loc) +let pr_dir dir = + let s,mp = + let open Nametab in + let open GlobDirRef in match dir with + | DirOpenModule mp -> "Open Module", ModPath.print mp + | DirOpenModtype mp -> "Open Module Type", ModPath.print mp + | DirOpenSection dir -> "Open Section", pr_path dir + in + str s ++ spc () ++ mp + let pr_located_qualid env = function | Term ref -> let ref_str = let open GlobRef in match ref with @@ -949,15 +959,7 @@ let pr_located_qualid env = function v 0 (hov 0 (str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) ++ extra)) | Abbreviation kn -> str "Notation" ++ spc () ++ pr_path (Nametab.path_of_abbreviation kn) - | Dir dir -> - let s,mp = - let open Nametab in - let open GlobDirRef in match dir with - | DirOpenModule mp -> "Open Module", ModPath.print mp - | DirOpenModtype mp -> "Open Module Type", ModPath.print mp - | DirOpenSection dir -> "Open Section", pr_path dir - in - str s ++ spc () ++ mp + | Dir dir -> pr_dir dir | Module mp -> str "Module" ++ spc () ++ pr_path (Nametab.path_of_module mp) | ModuleType mp -> @@ -980,7 +982,7 @@ let print_any_name access env sigma na udecl = | Term gref -> print_global_reference access env sigma gref udecl | Abbreviation kn -> print_abbreviation access env sigma kn | Module mp -> print_module mp - | Dir _ -> mt () + | Dir dir -> pr_dir dir | ModuleType mp -> print_modtype mp | Other (obj, info) -> info.print obj | Undefined qid -> diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml index 2daf83bca0ee..555a1175df3d 100644 --- a/vernac/vernac_classifier.ml +++ b/vernac/vernac_classifier.ml @@ -83,7 +83,7 @@ let classify_vernac e = (* Plugins should classify their commands *) | VernacLoad _ -> VtSideff ([], VtNow) | VernacExtend (s,l) -> - try Vernacextend.get_vernac_classifier s l + try Vernacextend.get_vernac_classifier s ~atts l with Not_found -> anomaly(str"No classifier for"++spc()++str s.ext_entry ++str".") in let static_pure_classifier ~atts e = match e with diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 497410556d26..ef2f853c501e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -554,7 +554,7 @@ let mk_sources () = let edges = let libs = Library.loaded_libraries () in List.fold_left (fun edges dp -> - let _, csts = Safe_typing.univs_of_library @@ Library.library_compiled dp in + let _, (_, csts) = Safe_typing.univs_of_library @@ Library.library_compiled dp in Constraints.fold (fun cst edges -> add_edge cst (Library dp) edges) csts edges) edges libs diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 98ce0b10aa86..c61ca1ced211 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -92,7 +92,10 @@ let type_vernac opn converted_args ?loc ~atts = (** VERNAC EXTEND registering *) -type classifier = Genarg.raw_generic_argument list -> vernac_classification +type classifier = + Genarg.raw_generic_argument list -> + atts:Attributes.vernac_flags -> + vernac_classification (** Classifiers *) module StringPair = @@ -119,7 +122,7 @@ let classify_as_sideeff = VtSideff ([], VtLater) let classify_as_proofstep = VtProofStep { proof_block_detection = None} type (_, _) ty_sig = -| TyNil : (vernac_command, vernac_classification) ty_sig +| TyNil : (vernac_command, atts:Attributes.vernac_flags -> vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig @@ -199,7 +202,7 @@ let static_vernac_extend ~plugin ~command ?classifier ?entry ext = | Some cl -> untype_classifier ty cl | None -> match classifier with - | Some cl -> fun _ -> cl command + | Some cl -> fun _ ~atts -> cl ~atts command | None -> let e = match entry with | None -> "COMMAND" diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 8794e197c85f..6d68bcc88d01 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -75,10 +75,13 @@ val type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command (** {5 VERNAC EXTEND} *) -type classifier = Genarg.raw_generic_argument list -> vernac_classification +type classifier = + Genarg.raw_generic_argument list -> + atts:Attributes.vernac_flags -> + vernac_classification type (_, _) ty_sig = -| TyNil : (vernac_command, vernac_classification) ty_sig +| TyNil : (vernac_command, atts:Attributes.vernac_flags -> vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> @@ -100,7 +103,7 @@ type ty_ml = TyML : bool (* deprecated *) * ('r, 's) ty_sig * 'r * 's option -> val static_vernac_extend : plugin:string option -> command:string -> - ?classifier:(string -> vernac_classification) -> + ?classifier:(atts:Attributes.vernac_flags -> string -> vernac_classification) -> ?entry:Vernacexpr.vernac_expr Procq.Entry.t -> ty_ml list -> unit