diff options
120 files changed, 1037 insertions, 459 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 56f48aaa4f..9e2af04e28 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -14,7 +14,7 @@ /configure* @coq/legacy-build-maintainers @coq/build-maintainers -/META.coq.in @coq/legacy-build-maintainers +/META.coq-core.in @coq/legacy-build-maintainers ########## CI infrastructure ########## diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f5527192e0..7ec3ba1bd7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -63,18 +63,18 @@ jobs: MACOSX_DEPLOYMENT_TARGET: "10.11" NJOBS: "2" + - name: Install Coq + run: | + make install install-byte + - name: Run Coq Test Suite run: | eval $(opam env) - export OCAMLPATH=$(pwd):"$OCAMLPATH" + export OCAMLPATH="$(pwd)/_install_ci/lib":"$OCAMLPATH" make -j "$NJOBS" test-suite PRINT_LOGS=1 env: NJOBS: "2" - - name: Install Coq - run: | - make install - - name: Create the dmg bundle run: | eval $(opam env) diff --git a/.gitignore b/.gitignore index 7d05a12cfe..bf7430cc2e 100644 --- a/.gitignore +++ b/.gitignore @@ -184,6 +184,7 @@ plugins/ssr/ssrvernac.ml # ocaml dev files .merlin META.coq +META.coq-core # Files automatically generated by Dune. *.install diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 14bf263251..d0ffedab2a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -375,7 +375,8 @@ pkg:opam: # OPAM will build out-of-tree so no point in importing artifacts script: - set -e - - opam pin add --kind=path coq.dev . + - opam pin add --kind=path coq-core.dev . + - opam pin add --kind=path coq-stdlib.dev . - opam pin add --kind=path coqide-server.dev . - opam pin add --kind=path coqide.dev . - set +e diff --git a/META.coq.in b/META.coq-core.in index 39e35561ff..c58513979d 100644 --- a/META.coq.in +++ b/META.coq-core.in @@ -35,7 +35,7 @@ package "lib" ( directory = "lib" - requires = "coq.clib, coq.config, dynlink" + requires = "coq-core.clib, coq-core.config, dynlink" archive(byte) = "lib.cma" archive(native) = "lib.cmxa" @@ -68,7 +68,7 @@ package "kernel" ( directory = "kernel" - requires = "coq.lib, coq.vm" + requires = "coq-core.lib, coq-core.vm" archive(byte) = "kernel.cma" archive(native) = "kernel.cmxa" @@ -80,7 +80,7 @@ package "library" ( description = "Coq Libraries (vo) support" version = "8.14" - requires = "coq.kernel" + requires = "coq-core.kernel" directory = "library" @@ -94,7 +94,7 @@ package "engine" ( description = "Coq Tactic Engine" version = "8.14" - requires = "coq.library" + requires = "coq-core.library" directory = "engine" archive(byte) = "engine.cma" @@ -107,7 +107,7 @@ package "pretyping" ( description = "Coq Pretyper" version = "8.14" - requires = "coq.engine" + requires = "coq-core.engine" directory = "pretyping" archive(byte) = "pretyping.cma" @@ -120,7 +120,7 @@ package "interp" ( description = "Coq Term Interpretation" version = "8.14" - requires = "zarith, coq.pretyping" + requires = "zarith, coq-core.pretyping" directory = "interp" archive(byte) = "interp.cma" @@ -133,7 +133,7 @@ package "proofs" ( description = "Coq Proof Engine" version = "8.14" - requires = "coq.interp" + requires = "coq-core.interp" directory = "proofs" archive(byte) = "proofs.cma" @@ -146,7 +146,7 @@ package "gramlib" ( description = "Coq Grammar Engine" version = "8.14" - requires = "coq.lib" + requires = "coq-core.lib" directory = "gramlib/.pack" archive(byte) = "gramlib.cma" @@ -158,7 +158,7 @@ package "parsing" ( description = "Coq Parsing Engine" version = "8.14" - requires = "coq.gramlib, coq.proofs" + requires = "coq-core.gramlib, coq-core.proofs" directory = "parsing" archive(byte) = "parsing.cma" @@ -171,7 +171,7 @@ package "printing" ( description = "Coq Printing Engine" version = "8.14" - requires = "coq.parsing" + requires = "coq-core.parsing" directory = "printing" archive(byte) = "printing.cma" @@ -184,7 +184,7 @@ package "tactics" ( description = "Coq Basic Tactics" version = "8.14" - requires = "coq.printing" + requires = "coq-core.printing" directory = "tactics" archive(byte) = "tactics.cma" @@ -197,7 +197,7 @@ package "vernac" ( description = "Coq Vernacular Interpreter" version = "8.14" - requires = "coq.tactics" + requires = "coq-core.tactics" directory = "vernac" archive(byte) = "vernac.cma" @@ -210,7 +210,7 @@ package "stm" ( description = "Coq State Transaction Machine" version = "8.14" - requires = "coq.sysinit" + requires = "coq-core.sysinit" directory = "stm" archive(byte) = "stm.cma" @@ -223,7 +223,7 @@ package "sysinit" ( description = "Coq initialization" version = "8.14" - requires = "coq.vernac" + requires = "coq-core.vernac" directory = "sysinit" archive(byte) = "sysinit.cma" @@ -236,7 +236,7 @@ package "toplevel" ( description = "Coq Toplevel" version = "8.14" - requires = "coq.stm" + requires = "coq-core.stm" directory = "toplevel" archive(byte) = "toplevel.cma" @@ -249,7 +249,7 @@ package "idetop" ( description = "Coq IDE Libraries" version = "8.14" - requires = "coq.toplevel" + requires = "coq-core.toplevel" directory = "ide" archive(byte) = "coqidetop.cma" @@ -262,7 +262,7 @@ package "ide" ( description = "Coq IDE Libraries" version = "8.14" - requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3" + requires = "coq-core.lib, coq-core.ideprotocol, lablgtk3, lablgtk3-sourceview3" directory = "ide" archive(byte) = "ide.cma" @@ -275,7 +275,7 @@ package "ideprotocol" ( description = "Coq IDE protocol" version = "8.14" - requires = "coq.toplevel" + requires = "coq-core.toplevel" directory = "ide/protocol" archive(byte) = "ideprotocol.cma" @@ -295,7 +295,7 @@ package "plugins" ( description = "Coq LTAC Plugin" version = "8.14" - requires = "coq.stm" + requires = "coq-core.stm" directory = "ltac" archive(byte) = "ltac_plugin.cmo" @@ -310,7 +310,7 @@ package "plugins" ( description = "Coq tauto plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "ltac" archive(byte) = "tauto_plugin.cmo" @@ -325,7 +325,7 @@ package "plugins" ( description = "Coq omega plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "omega" archive(byte) = "omega_plugin.cmo" @@ -340,7 +340,7 @@ package "plugins" ( description = "Coq micromega plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "micromega" archive(byte) = "micromega_plugin.cmo" @@ -355,7 +355,7 @@ package "plugins" ( description = "Coq Zify plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "micromega" archive(byte) = "zify_plugin.cmo" @@ -385,7 +385,7 @@ package "plugins" ( description = "Coq extraction plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "extraction" archive(byte) = "extraction_plugin.cmo" @@ -400,7 +400,7 @@ package "plugins" ( description = "Coq cc plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "cc" archive(byte) = "cc_plugin.cmo" @@ -415,7 +415,7 @@ package "plugins" ( description = "Coq ground plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "firstorder" archive(byte) = "ground_plugin.cmo" @@ -430,7 +430,7 @@ package "plugins" ( description = "Coq rtauto plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "rtauto" archive(byte) = "rtauto_plugin.cmo" @@ -445,7 +445,7 @@ package "plugins" ( description = "Coq btauto plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "btauto" archive(byte) = "btauto_plugin.cmo" @@ -460,7 +460,7 @@ package "plugins" ( description = "Coq recdef plugin" version = "8.14" - requires = "coq.plugins.extraction" + requires = "coq-core.plugins.extraction" directory = "funind" archive(byte) = "recdef_plugin.cmo" @@ -475,7 +475,7 @@ package "plugins" ( description = "Coq nsatz plugin" version = "8.14" - requires = "zarith, coq.plugins.ltac" + requires = "zarith, coq-core.plugins.ltac" directory = "nsatz" archive(byte) = "nsatz_plugin.cmo" @@ -505,7 +505,7 @@ package "plugins" ( description = "Coq string_notation plugin" version = "8.14" - requires = "coq.vernac" + requires = "coq-core.vernac" directory = "syntax" archive(byte) = "string_notation_plugin.cmo" @@ -519,7 +519,7 @@ package "plugins" ( description = "Coq numeral notation plugin" version = "8.14" - requires = "coq.vernac" + requires = "coq-core.vernac" directory = "numeral_notation" archive(byte) = "numeral_notation_plugin.cmo" @@ -549,7 +549,7 @@ package "plugins" ( description = "Coq ssrmatching plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "ssrmatching" archive(byte) = "ssrmatching_plugin.cmo" @@ -564,7 +564,7 @@ package "plugins" ( description = "Coq ssreflect plugin" version = "8.14" - requires = "coq.plugins.ssrmatching" + requires = "coq-core.plugins.ssrmatching" directory = "ssr" archive(byte) = "ssreflect_plugin.cmo" @@ -579,7 +579,7 @@ package "plugins" ( description = "Coq Ltac2 Plugin" version = "8.14" - requires = "coq.plugins.ltac" + requires = "coq-core.plugins.ltac" directory = "../user-contrib/Ltac2" archive(byte) = "ltac2_plugin.cmo" diff --git a/Makefile.dune b/Makefile.dune index c2899dcaba..c338405f2c 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -56,7 +56,8 @@ help-install: @echo "" @echo " Provided opam/dune packages are:" @echo "" - @echo " - coq: base Coq package, toplevel compilers, tools, stdlib, no GTK" + @echo " - coq-core: base Coq package, toplevel compilers, plugins, tools, no stdlib, no GTK" + @echo " - coq-stdlib: Coq's standard library" @echo " - coqide-server: XML protocol language server" @echo " - coqide: CoqIDE gtk application" @echo "" @@ -82,7 +83,7 @@ voboot: states: dune build $(DUNEOPT) dev/shim/coqtop-prelude -NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install +NONDOC_INSTALL_TARGETS:=coq-core.install coq-stdlib.install coqide-server.install coqide.install world: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) diff --git a/Makefile.install b/Makefile.install index 4977bb38e1..0dd4c1bc24 100644 --- a/Makefile.install +++ b/Makefile.install @@ -162,8 +162,9 @@ install-latex: $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) # -$(UPDATETEX) -install-meta: META.coq - $(INSTALLLIB) META.coq $(FULLCOQLIB)/META +install-meta: META.coq-core + $(INSTALLLIB) META.coq-core $(FULLCOQLIB)/META + cd $(FULLCOQLIB)/.. && rm -f coq-core && ln -s coq coq-core # For emacs: # Local Variables: diff --git a/Makefile.make b/Makefile.make index 5e45e71c8c..9f0e06dffc 100644 --- a/Makefile.make +++ b/Makefile.make @@ -187,10 +187,10 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### # OCaml dev files ########################################################################### -camldevfiles: $(MERLINFILES) META.coq +camldevfiles: $(MERLINFILES) META.coq-core # prevent submake dependency -META.coq.in $(MERLININFILES): ; +META.coq-core.in $(MERLININFILES): ; .merlin: .merlin.in cp -a "$<" "$@" @@ -198,7 +198,7 @@ META.coq.in $(MERLININFILES): ; %/.merlin: %/.merlin.in cp -a "$<" "$@" -META.coq: META.coq.in +META.coq-core: META.coq-core.in cp -a "$<" "$@" ########################################################################### @@ -222,7 +222,7 @@ cruftclean: mlgclean rm -f gmon.out core camldevfilesclean: - rm -f $(MERLINFILES) META.coq + rm -f $(MERLINFILES) META.coq-core indepclean: rm -f $(GENFILES) diff --git a/checker/checker.ml b/checker/checker.ml index ba5e3c6d1a..f55ed9e8d6 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -107,7 +107,15 @@ let init_load_path () = let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs in let coqpath = Envars.coqpath in - let plugins = coqlib/"plugins" in + let plugins = + CPath.choose_existing + [ CPath.make [ coqlib ; "plugins" ] + ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] + ] |> function + | None -> + CErrors.user_err (Pp.str "Cannot find plugins directory") + | Some f -> (f :> string) + in (* NOTE: These directories are searched from last to first *) (* first standard library *) add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]); diff --git a/checker/dune b/checker/dune index af7d4f2923..78b4032141 100644 --- a/checker/dune +++ b/checker/dune @@ -7,13 +7,14 @@ (synopsis "Coq's Standalone Proof Checker") (modules :standard \ coqchk votour) (wrapped true) - (libraries coq.kernel)) + (libraries coq-core.kernel)) (executable (name coqchk) (public_name coqchk) (modes exe byte) - (package coq) + ; Move to coq-checker? + (package coq-core) (modules coqchk) (flags :standard -open Coq_checklib) (libraries coq_checklib)) @@ -21,7 +22,7 @@ (executable (name votour) (public_name votour) - (package coq) + (package coq-core) (modules votour) (flags :standard -open Coq_checklib) (libraries coq_checklib)) diff --git a/clib/cPath.ml b/clib/cPath.ml new file mode 100644 index 0000000000..66d03078dc --- /dev/null +++ b/clib/cPath.ml @@ -0,0 +1,27 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* This API is loosely inspired by [Stdune.Path], for now we keep it + minimal, but at some point we may extend it, see developer notes in + the implementation file. *) + +type t = string + +(* Note that in general, make is not safe, due to its type, however + relative is as you can enforce a particular root. So we eventually + should remove [make] *) +let make = List.fold_left Filename.concat "" + +let relative = Filename.concat + +let rec choose_existing = function + | [] -> None + | f :: fs -> + if Sys.file_exists f then Some f else choose_existing fs diff --git a/clib/cPath.mli b/clib/cPath.mli new file mode 100644 index 0000000000..762279a218 --- /dev/null +++ b/clib/cPath.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* This API is loosely inspired by [Stdune.Path], for now we keep it + minimal, but at some point we may extend it, see developer notes in + the implementation file. *) + +(* To be made opaque one day, for now we force users to go thru the + constructor *) +type t = private string + +(** [make path_components] build a path from its components *) +val make : string list -> t + +(** [relative path string] build a path relative to an existing one *) +val relative : t -> string -> t + +(** [choose_existing paths] will return [Some f] for the first file + [f] in [paths] that exists, [None] otherwise. *) +val choose_existing : t list -> t option + +(* We should gradually add some more functions to handle common dirs + here such the theories directories or share files. Abstracting it + here does allow to use system-specific functionalities *) diff --git a/clib/clib.mllib b/clib/clib.mllib index be3b5971be..02f2ec8e56 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -37,3 +37,5 @@ Terminal Monad Diff2 + +CPath @@ -1,8 +1,7 @@ (library (name clib) (synopsis "Coq's Utility Library [general purpose]") - (public_name coq.clib) + (public_name coq-core.clib) (wrapped false) (modules_without_implementation cSig) (libraries str unix threads)) - diff --git a/config/dune b/config/dune index 83d1364b0c..777201f29f 100644 --- a/config/dune +++ b/config/dune @@ -1,7 +1,7 @@ (library (name config) (synopsis "Coq Configuration Variables") - (public_name coq.config) + (public_name coq-core.config) (modules :standard \ list_plugins) (wrapped false)) diff --git a/configure.ml b/configure.ml index 7814204e42..abea59bd60 100644 --- a/configure.ml +++ b/configure.ml @@ -336,9 +336,16 @@ let arg_profile = Arg.String (fun s -> prefs := Profiles.get s !prefs) (* TODO : earlier any option -foo was also available as --foo *) +let check_absolute = function + | None -> () + | Some path -> + if Filename.is_relative path then + die "argument to -prefix must be an absolute path" + else () + let args_options = Arg.align [ - "-prefix", arg_string_option (fun p prefix -> { p with prefix }), - "<dir> Set installation directory to <dir>"; + "-prefix", arg_string_option (fun p prefix -> check_absolute prefix; { p with prefix }), + "<dir> Set installation directory to <dir> (absolute path required)"; "-local", arg_set (fun p local -> { p with local }), " Set installation directory to the current source tree"; "-no-ask", arg_clear (fun p interactive -> { p with interactive }), diff --git a/coq-core.opam b/coq-core.opam new file mode 100644 index 0000000000..8b8c43f66e --- /dev/null +++ b/coq-core.opam @@ -0,0 +1,54 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" +synopsis: "The Coq Proof Assistant -- Core Binaries and Tools" +description: """ +Coq is a formal proof management system. 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. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching. + +This package includes the Coq core binaries, plugins, and tools, but +not the vernacular standard library. + +Note that in this setup, Coq needs to be started with the -boot and +-noinit options, as will otherwise fail to find the regular Coq +prelude, now living in the coq-stdlib package.""" +maintainer: ["The Coq development team <coqdev@inria.fr>"] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" +homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" +bug-reports: "https://github.com/coq/coq/issues" +depends: [ + "dune" {>= "2.5"} + "ocaml" {>= "4.05.0"} + "ocamlfind" {>= "1.8.1"} + "zarith" {>= "1.10"} + "ounit2" {with-test} +] +build: [ + # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 + # ["dune" "subst"] {pinned} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq/coq.git" +build-env: [ + [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] +] diff --git a/coq.opam.template b/coq-core.opam.template index c0efccdc0f..c0efccdc0f 100644 --- a/coq.opam.template +++ b/coq-core.opam.template diff --git a/coq-doc.opam b/coq-doc.opam index 9b0d562c45..37bf1e95fe 100644 --- a/coq-doc.opam +++ b/coq-doc.opam @@ -21,8 +21,8 @@ depends: [ "coq" {build & = version} ] build: [ -# Disabled until Dune 2.8 is available -# ["dune" "subst"] {pinned} + # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 + # ["dune" "subst"] {pinned} [ "dune" "build" diff --git a/coq-stdlib.opam b/coq-stdlib.opam new file mode 100644 index 0000000000..20d994abcb --- /dev/null +++ b/coq-stdlib.opam @@ -0,0 +1,44 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" +synopsis: "The Coq Proof Assistant -- Standard Library" +description: """ +Coq is a formal proof management system. 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. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching. + +This package includes the Coq Standard Library, that is to say, the +set of modules usually bound to the Coq.* namespace.""" +maintainer: ["The Coq development team <coqdev@inria.fr>"] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" +homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" +bug-reports: "https://github.com/coq/coq/issues" +depends: [ + "dune" {>= "2.5"} + "coq-core" {= version} +] +build: [ + # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 + # ["dune" "subst"] {pinned} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq/coq.git" @@ -20,15 +20,12 @@ homepage: "https://coq.inria.fr/" doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" depends: [ - "ocaml" {>= "4.05.0"} - "dune" {>= "2.5.0"} - "ocamlfind" {>= "1.8.1"} - "zarith" {>= "1.10"} - "ounit2" {with-test} + "dune" {>= "2.5"} + "coq-core" {= version} + "coq-stdlib" {= version} ] build: [ -# Disabled until Dune 2.8 is available -# ["dune" "subst"] {pinned} + ["dune" "subst"] {pinned} [ "dune" "build" @@ -42,6 +39,3 @@ build: [ ] ] dev-repo: "git+https://github.com/coq/coq.git" -build-env: [ - [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] -] diff --git a/coqide-server.opam b/coqide-server.opam index cbb0db2893..8359b5f04e 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -19,12 +19,12 @@ homepage: "https://coq.inria.fr/" doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" depends: [ - "dune" {>= "2.5.0"} - "coq" {= version} + "dune" {>= "2.5"} + "coq-core" {= version} ] build: [ -# Disabled until Dune 2.8 is available -# ["dune" "subst"] {pinned} + # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 + # ["dune" "subst"] {pinned} [ "dune" "build" diff --git a/coqide.opam b/coqide.opam index 9e4fb05701..3c59f7fd9c 100644 --- a/coqide.opam +++ b/coqide.opam @@ -17,12 +17,12 @@ homepage: "https://coq.inria.fr/" doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" depends: [ - "dune" {>= "2.5.0"} + "dune" {>= "2.5"} "coqide-server" {= version} ] build: [ -# Disabled until Dune 2.8 is available -# ["dune" "subst"] {pinned} + # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 + # ["dune" "subst"] {pinned} [ "dune" "build" diff --git a/coqpp/dune b/coqpp/dune index d4b49301fb..e4cdc33b3d 100644 --- a/coqpp/dune +++ b/coqpp/dune @@ -10,6 +10,6 @@ (executable (name coqpp_main) (public_name coqpp) - (package coq) + (package coq-core) (libraries coqpp) (modules coqpp_main)) diff --git a/default.nix b/default.nix index 0b23bdb48c..f838f17d07 100644 --- a/default.nix +++ b/default.nix @@ -98,7 +98,7 @@ stdenv.mkDerivation rec { createFindlibDestdir = !shell; - postInstall = "ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq"; + postInstall = "ln -s $out/lib/coq-core $OCAMLFIND_DESTDIR/coq-core"; inherit doInstallCheck; diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 569977f76b..49c8099e8b 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -283,25 +283,27 @@ create_opam() { echo "$1_coq_commit_long = $COQ_HASH_LONG" - _RES=0 - /usr/bin/time -o "$log_dir/coq.$RUNNER.1.time" --format="%U %M %F" \ - perf stat -e instructions:u,cycles:u -o "$log_dir/coq.$RUNNER.1.perf" \ - opam pin add -y -b -j "$number_of_processors" --kind=path coq.dev . \ - 3>$log_dir/coq.$RUNNER.opam_install.1.stdout.log 1>&3 \ - 4>$log_dir/coq.$RUNNER.opam_install.1.stderr.log 2>&4 || \ - _RES=$? - if [ $_RES = 0 ]; then - echo "Coq ($RUNNER) installed successfully" - else - echo "ERROR: \"opam install coq.$coq_opam_version\" has failed (for the $RUNNER commit = $COQ_HASH_LONG)." - exit 1 - fi + for package in coq-core coq-stdlib coq; do + _RES=0 + /usr/bin/time -o "$log_dir/$package.$RUNNER.1.time" --format="%U %M %F" \ + perf stat -e instructions:u,cycles:u -o "$log_dir/$package.$RUNNER.1.perf" \ + opam pin add -y -b -j "$number_of_processors" --kind=path $package.dev . \ + 3>$log_dir/$package.$RUNNER.opam_install.1.stdout.log 1>&3 \ + 4>$log_dir/$package.$RUNNER.opam_install.1.stderr.log 2>&4 || \ + _RES=$? + if [ $_RES = 0 ]; then + echo "$package ($RUNNER) installed successfully" + else + echo "ERROR: \"opam install $package.$coq_opam_version\" has failed (for the $RUNNER commit = $COQ_HASH_LONG)." + exit 1 + fi - # we don't multi compile coq for now (TODO some other time) - # the render needs all the files so copy them around - for it in $(seq 2 $num_of_iterations); do - cp "$log_dir/coq.$RUNNER.1.time" "$log_dir/coq.$RUNNER.$it.time" - cp "$log_dir/coq.$RUNNER.1.perf" "$log_dir/coq.$RUNNER.$it.perf" + # we don't multi compile coq for now (TODO some other time) + # the render needs all the files so copy them around + for it in $(seq 2 $num_of_iterations); do + cp "$log_dir/$package.$RUNNER.1.time" "$log_dir/$package.$RUNNER.$it.time" + cp "$log_dir/$package.$RUNNER.1.perf" "$log_dir/$package.$RUNNER.$it.perf" + done done } @@ -327,7 +329,7 @@ fi export TIMING=1 # The following variable will be set in the following cycle: -installable_coq_opam_packages=coq +installable_coq_opam_packages="coq-core coq-stdlib coq" for coq_opam_package in $sorted_coq_opam_packages; do diff --git a/dev/ci/user-overlays/13842-proux01-remove-decimal.sh b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh new file mode 100644 index 0000000000..5ede8221ce --- /dev/null +++ b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh @@ -0,0 +1 @@ +overlay hott https://github.com/proux01/HoTT coq-13842 13842 @@ -1,11 +1,11 @@ (library (name top_printers) - (public_name coq.top_printers) + (public_name coq-core.top_printers) (synopsis "Coq's Debug Printers") (wrapped false) (modules top_printers) (optional) - (libraries coq.toplevel coq.plugins.ltac)) + (libraries coq-core.toplevel coq-core.plugins.ltac)) (rule (targets dune-dbg) @@ -17,27 +17,27 @@ ; We require all the OCaml libs to be in place and searchable ; by OCamlfind, this is a bit of a hack but until Dune gets ; proper ocamldebug support we have to live with that. - %{lib:coq.config:config.cma} - %{lib:coq.clib:clib.cma} - %{lib:coq.lib:lib.cma} - %{lib:coq.kernel:kernel.cma} - %{lib:coq.vm:byterun.cma} - %{lib:coq.vm:../../stublibs/dllbyterun_stubs.so} - %{lib:coq.library:library.cma} - %{lib:coq.engine:engine.cma} - %{lib:coq.pretyping:pretyping.cma} - %{lib:coq.gramlib:gramlib.cma} - %{lib:coq.interp:interp.cma} - %{lib:coq.proofs:proofs.cma} - %{lib:coq.parsing:parsing.cma} - %{lib:coq.printing:printing.cma} - %{lib:coq.tactics:tactics.cma} - %{lib:coq.vernac:vernac.cma} - %{lib:coq.stm:stm.cma} - %{lib:coq.sysinit:sysinit.cma} - %{lib:coq.toplevel:toplevel.cma} - %{lib:coq.plugins.ltac:ltac_plugin.cma} - %{lib:coq.top_printers:top_printers.cmi} - %{lib:coq.top_printers:top_printers.cma} - %{lib:coq.top_printers:../META}) + %{lib:coq-core.config:config.cma} + %{lib:coq-core.clib:clib.cma} + %{lib:coq-core.lib:lib.cma} + %{lib:coq-core.kernel:kernel.cma} + %{lib:coq-core.vm:byterun.cma} + %{lib:coq-core.vm:../../stublibs/dllbyterun_stubs.so} + %{lib:coq-core.library:library.cma} + %{lib:coq-core.engine:engine.cma} + %{lib:coq-core.pretyping:pretyping.cma} + %{lib:coq-core.gramlib:gramlib.cma} + %{lib:coq-core.interp:interp.cma} + %{lib:coq-core.proofs:proofs.cma} + %{lib:coq-core.parsing:parsing.cma} + %{lib:coq-core.printing:printing.cma} + %{lib:coq-core.tactics:tactics.cma} + %{lib:coq-core.vernac:vernac.cma} + %{lib:coq-core.stm:stm.cma} + %{lib:coq-core.sysinit:sysinit.cma} + %{lib:coq-core.toplevel:toplevel.cma} + %{lib:coq-core.plugins.ltac:ltac_plugin.cma} + %{lib:coq-core.top_printers:top_printers.cmi} + %{lib:coq-core.top_printers:top_printers.cma} + %{lib:coq-core.top_printers:../META}) (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/shim/dune b/dev/shim/dune index 8006c629ed..e4cc7699f0 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -26,7 +26,7 @@ (targets coqbyte-prelude) (deps %{bin:coqtop.byte} - %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so} + %{lib:coq-core.kernel:../../stublibs/dllbyterun_stubs.so} %{project_root}/theories/Init/Prelude.vo) (action (with-stdout-to %{targets} diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 5f9f326750..d4f599484f 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -33,7 +33,7 @@ (defun coqdev-default-directory () "Return the Coq repository containing `default-directory'." - (let ((dir (locate-dominating-file default-directory "META.coq.in"))) + (let ((dir (locate-dominating-file default-directory "META.coq-core.in"))) (when dir (expand-file-name dir)))) (defun coqdev-setup-compile-command () diff --git a/doc/changelog/03-notations/13842-remove-decimal.rst b/doc/changelog/03-notations/13842-remove-decimal.rst new file mode 100644 index 0000000000..4bc26ef6a8 --- /dev/null +++ b/doc/changelog/03-notations/13842-remove-decimal.rst @@ -0,0 +1,3 @@ +- **Removed:** + Remove decimal-only number notations which were deprecated in 8.12. + (`#13842 <https://github.com/coq/coq/pull/13842>`_, by Pierre Roux). diff --git a/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst b/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst new file mode 100644 index 0000000000..31b331f0ff --- /dev/null +++ b/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Setoid rewriting now remembers the (invisible) binder names of non-dependent product types. SSReflect's rewrite tactic expects these names to be retained when using ``rewrite foo in H``. + This also fixes SSR ``rewrite foo in H *`` erroneously reverting ``H``. + (`#13882 <https://github.com/coq/coq/pull/13882>`_, + fixes `#12011 <https://github.com/coq/coq/issues/12011>`_, + by Gaëtan Gilbert). diff --git a/doc/changelog/05-tactic-language/13236-ltac2-printf.rst b/doc/changelog/05-tactic-language/13236-ltac2-printf.rst new file mode 100644 index 0000000000..02213f22e5 --- /dev/null +++ b/doc/changelog/05-tactic-language/13236-ltac2-printf.rst @@ -0,0 +1,7 @@ +- **Added:** + Added a ``printf`` macro to Ltac2. It can be made accessible by + importing the ``Ltac2.Printf`` module. See the documentation + there for more information + (`#13236 <https://github.com/coq/coq/pull/13236>`_, + fixes `#10108 <https://github.com/coq/coq/issues/10108>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst b/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst new file mode 100644 index 0000000000..6fe6f62faa --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst @@ -0,0 +1,14 @@ +- **Changed:** + Coq's configure script now requires absolute paths for the `-prefix` + option. + (`#12567 <https://github.com/coq/coq/pull/12567>`_, + by Emilio Jesus Gallego Arias). + +- **Changed:** + The regular Coq package has been split in two: coq-core, with + OCaml-based libraries and tools; and coq-stdlib, which contains the + Gallina-based standard library. The package Coq now depends on both + for compatiblity. + (`#12567 <https://github.com/coq/coq/pull/12567>`_, + by Emilio Jesus Gallego Arias, review by Vincent Laporte, Guillaume + Melquiond, Enrico Tassi, and Théo Zimmerman). diff --git a/doc/changelog/12-misc/13586-nested-timeout.rst b/doc/changelog/12-misc/13586-nested-timeout.rst new file mode 100644 index 0000000000..2c31dc210a --- /dev/null +++ b/doc/changelog/12-misc/13586-nested-timeout.rst @@ -0,0 +1,7 @@ +- **Fixed:** + Fix the timeout facility on Unix to allow for nested timeouts. + Previous behavior on nested timeouts was that an "inner" timeout would replace an "outer" + timeout, so that the outer timeout would no longer fire. With the new behavior, Unix and Windows + implementations should be (approximately) equivalent. + (`#13586 <https://github.com/coq/coq/pull/13586>`_, + by Lasse Blaauwbroek). @@ -13,7 +13,8 @@ ; + %{bin:coqdoc} etc... ; + config/coq_config.py ; + tools/coqdoc/coqdoc.css - (package coq) + (package coq-core) + (package coq-stdlib) (source_tree sphinx) (source_tree tools/coqrst) unreleased.rst @@ -26,7 +27,8 @@ ; Cannot use this deps alias because of ocaml/dune#3415 ; (deps (alias refman-deps)) (deps - (package coq) + (package coq-core) + (package coq-stdlib) (source_tree sphinx) (source_tree tools/coqrst) unreleased.rst @@ -41,7 +43,8 @@ ; Cannot use this deps alias because of ocaml/dune#3415 ; (deps (alias refman-deps)) (deps - (package coq) + (package coq-core) + (package coq-stdlib) (source_tree sphinx) (source_tree tools/coqrst) unreleased.rst diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune index ab9b4dd531..c7ed997221 100644 --- a/doc/plugin_tutorial/tuto0/src/dune +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -1,6 +1,6 @@ (library (name tuto0_plugin) - (public_name coq.plugins.tutorial.p0) - (libraries coq.plugins.ltac)) + (public_name coq-core.plugins.tutorial.p0) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_tuto0)) diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune index 054d5ecd26..bf87222e16 100644 --- a/doc/plugin_tutorial/tuto1/src/dune +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -1,6 +1,6 @@ (library (name tuto1_plugin) - (public_name coq.plugins.tutorial.p1) - (libraries coq.plugins.ltac)) + (public_name coq-core.plugins.tutorial.p1) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_tuto1)) diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune index 8c4b04b1ae..0797debccf 100644 --- a/doc/plugin_tutorial/tuto2/src/dune +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -1,6 +1,6 @@ (library (name tuto2_plugin) - (public_name coq.plugins.tutorial.p2) - (libraries coq.plugins.ltac)) + (public_name coq-core.plugins.tutorial.p2) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_tuto2)) diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune index 678dd71328..dcecf0852e 100644 --- a/doc/plugin_tutorial/tuto3/src/dune +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -1,7 +1,7 @@ (library (name tuto3_plugin) - (public_name coq.plugins.tutorial.p3) + (public_name coq-core.plugins.tutorial.p3) (flags :standard -warn-error -3) - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_tuto3)) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 2ea8694ad6..4f3ee2dcaf 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -82,13 +82,13 @@ Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann. -The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric +The 51 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, Cyril Cohen, Julien Coolen, Matthew Dempsky, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesús Gallego Arias, Paolo G. Giarrusso, Attila Gáspár, Gaëtan Gilbert, Jason Gross, Benjamin Grégoire, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Ignat Insarov, Ralf Jung, Fabian Kunze, Vincent Laporte, Olivier Laurent, Larry D. Lee Jr, -Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet, +Thomas Letan, Yishuai Li, James Lottes, Jean-Christophe Léchenet, Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond, Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau, diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 03571ad680..557ef10555 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1726,12 +1726,6 @@ Number notations * :n:`@qualid__type -> Number.number` * :n:`@qualid__type -> option Number.number` - .. deprecated:: 8.12 - Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and - :g:`Decimal.decimal` are replaced respectively by number - notations on :g:`Number.uint`, :g:`Number.int` and - :g:`Number.number`. - When parsing, the application of the parsing function :n:`@qualid__parse` to the number will be fully reduced, and universes of the resulting term will be refreshed. diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 0b6ca5f178..6b51202f6e 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -22,7 +22,8 @@ (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) ; For .glob files, should be gone when Coq Dune is smarter. - (package coq)) + (package coq-core) + (package coq-stdlib)) (action (progn (run mkdir -p html) diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 27eb64a83b..b0f4e883be 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -692,6 +692,7 @@ through the <tt>Require Import</tt> command.</p> user-contrib/Ltac2/Notations.v user-contrib/Ltac2/Option.v user-contrib/Ltac2/Pattern.v + user-contrib/Ltac2/Printf.v user-contrib/Ltac2/Std.v user-contrib/Ltac2/String.v </dd> diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 1c07d00d4f..4ba60ddd9f 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -1,6 +1,6 @@ (executable (name doc_grammar) - (libraries coq.clib coqpp)) + (libraries coq-core.clib coqpp)) (env (_ (binaries doc_grammar.exe))) @@ -20,7 +20,7 @@ (install (section lib) - (package coq) + (package coq-core) (files revision)) (rule diff --git a/dune-project b/dune-project index 03e7147019..251fbd92aa 100644 --- a/dune-project +++ b/dune-project @@ -22,14 +22,13 @@ ; Note that we use coq.opam.template to have dune add the correct opam ; prefix for configure (package - (name coq) + (name coq-core) (depends (ocaml (>= 4.05.0)) - (dune (>= 2.5.0)) (ocamlfind (>= 1.8.1)) (zarith (>= 1.10)) (ounit2 :with-test)) - (synopsis "The Coq Proof Assistant") + (synopsis "The Coq Proof Assistant -- Core Binaries and Tools") (description "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for @@ -39,13 +38,38 @@ Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the -Feit-Thompson theorem or homotopy type theory) and teaching.")) +Feit-Thompson theorem or homotopy type theory) and teaching. + +This package includes the Coq core binaries, plugins, and tools, but +not the vernacular standard library. + +Note that in this setup, Coq needs to be started with the -boot and +-noinit options, as will otherwise fail to find the regular Coq +prelude, now living in the coq-stdlib package.")) + +(package + (name coq-stdlib) + (depends + (coq-core (= :version))) + (synopsis "The Coq Proof Assistant -- Standard Library") + (description "Coq is a formal proof management system. 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. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching. + +This package includes the Coq Standard Library, that is to say, the +set of modules usually bound to the Coq.* namespace.")) (package (name coqide-server) (depends - (dune (>= 2.5.0)) - (coq (= :version))) + (coq-core (= :version))) (synopsis "The Coq Proof Assistant, XML protocol server") (description "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable @@ -60,7 +84,6 @@ structured way.")) (package (name coqide) (depends - (dune (>= 2.5.0)) (coqide-server (= :version))) (synopsis "The Coq Proof Assistant --- GTK3 IDE") (description "Coq is a formal proof management system. It provides @@ -86,3 +109,19 @@ semi-interactive development of machine-checked proofs. This package provides the Coq Reference Manual.")) +(package + (name coq) + (depends + (coq-core (= :version)) + (coq-stdlib (= :version))) + (synopsis "The Coq Proof Assistant") + (description "Coq is a formal proof management system. 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. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching.")) diff --git a/engine/dune b/engine/dune index e2b7ab9c87..00db94389b 100644 --- a/engine/dune +++ b/engine/dune @@ -1,6 +1,6 @@ (library (name engine) (synopsis "Coq's Tactic Engine") - (public_name coq.engine) + (public_name coq-core.engine) (wrapped false) (libraries library)) diff --git a/gramlib/dune b/gramlib/dune index 8ca6aff25a..62c64b0c1a 100644 --- a/gramlib/dune +++ b/gramlib/dune @@ -1,4 +1,4 @@ (library (name gramlib) - (public_name coq.gramlib) - (libraries coq.lib)) + (public_name coq-core.gramlib) + (libraries coq-core.lib)) diff --git a/ide/coqide/dune b/ide/coqide/dune index 12bad7ebc4..4bb4672cd4 100644 --- a/ide/coqide/dune +++ b/ide/coqide/dune @@ -6,7 +6,7 @@ (public_name coqide-server.core) (wrapped false) (modules document) - (libraries coq.lib)) + (libraries coq-core.lib)) (executable (name fake_ide) @@ -20,7 +20,7 @@ (public_name coqidetop.opt) (package coqide-server) (modules idetop) - (libraries coq.toplevel coqide-server.protocol) + (libraries coq-core.toplevel coqide-server.protocol) (modes native byte) (link_flags -linkall)) diff --git a/ide/coqide/protocol/dune b/ide/coqide/protocol/dune index 801ceb20ec..f48c7de0c4 100644 --- a/ide/coqide/protocol/dune +++ b/ide/coqide/protocol/dune @@ -2,6 +2,6 @@ (name protocol) (public_name coqide-server.protocol) (wrapped false) - (libraries coq.lib)) + (libraries coq-core.lib)) (ocamllex xml_lexer) diff --git a/interp/dune b/interp/dune index 6d73d5724c..793ce48ea3 100644 --- a/interp/dune +++ b/interp/dune @@ -1,6 +1,6 @@ (library (name interp) (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]") - (public_name coq.interp) + (public_name coq-core.interp) (wrapped false) (libraries zarith pretyping)) diff --git a/interp/notation.ml b/interp/notation.ml index ed605c994d..4010c3487e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -557,9 +557,6 @@ type target_kind = | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *) | Number of number_ty (* Coq.Init.Number.number + uint + int *) - | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) - | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) - | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *) type string_target_kind = | ListByte @@ -872,30 +869,16 @@ let mkDecHex ind c n = match c with | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Decimal *) | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hexadecimal *) -exception NonDecimal - -let decimal_coqnumber_of_rawnum inds n = - if NumTok.Signed.classify n <> CDec then raise NonDecimal; - coqnumber_of_rawnum inds CDec n - let coqnumber_of_rawnum inds n = let c = NumTok.Signed.classify n in let n = coqnumber_of_rawnum inds c n in mkDecHex inds.number c n -let decimal_coquint_of_rawnum inds n = - if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal; - coquint_of_rawnum inds CDec (Some n) - let coquint_of_rawnum inds n = let c = NumTok.UnsignedNat.classify n in let n = coquint_of_rawnum inds c (Some n) in mkDecHex inds.uint c n -let decimal_coqint_of_rawnum inds n = - if NumTok.SignedNat.classify n <> CDec then raise NonDecimal; - coqint_of_rawnum inds CDec n - let coqint_of_rawnum inds n = let c = NumTok.SignedNat.classify n in let n = coqint_of_rawnum inds c n in @@ -950,23 +933,14 @@ let destDecHex c = match Constr.kind c with | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken -let decimal_rawnum_of_coqnumber c = - rawnum_of_coqnumber CDec c - let rawnum_of_coqnumber c = let cl, c = destDecHex c in rawnum_of_coqnumber cl c -let decimal_rawnum_of_coquint c = - rawnum_of_coquint CDec c - let rawnum_of_coquint c = let cl, c = destDecHex c in rawnum_of_coquint cl c -let decimal_rawnum_of_coqint c = - rawnum_of_coqint CDec c - let rawnum_of_coqint c = let cl, c = destDecHex c in rawnum_of_coqint cl c @@ -1084,22 +1058,13 @@ let interp o ?loc n = coqint_of_rawnum int_ty n | UInt int_ty, Some (SPlus, n) -> coquint_of_rawnum int_ty n - | DecimalInt int_ty, Some n -> - (try decimal_coqint_of_rawnum int_ty n - with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) - | DecimalUInt int_ty, Some (SPlus, n) -> - (try decimal_coquint_of_rawnum int_ty n - with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) | Z z_pos_ty, Some n -> z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n) | Int63 pos_neg_int63_ty, Some n -> interp_int63 ?loc pos_neg_int63_ty.pos_neg_int63_ty (NumTok.SignedNat.to_bigint n) - | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63 _), _ -> + | (Int _ | UInt _ | Z _ | Int63 _), _ -> no_such_prim_token "number" ?loc o.ty_name | Number number_ty, _ -> coqnumber_of_rawnum number_ty n - | Decimal number_ty, _ -> - (try decimal_coqnumber_of_rawnum number_ty n - with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) in let env = Global.env () in let sigma = Evd.from_env env in @@ -1124,9 +1089,6 @@ let uninterp o n = | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c) | (Int63 _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_coqpos_neg_int63 c) | (Number _, c) -> rawnum_of_coqnumber c - | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c) - | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c) - | (Decimal _, c) -> decimal_rawnum_of_coqnumber c end o n end diff --git a/interp/notation.mli b/interp/notation.mli index 77f245ae77..195f2a4416 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -146,9 +146,6 @@ type target_kind = | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *) | Number of number_ty (* Coq.Init.Number.number + uint + int *) - | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) - | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) - | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *) type string_target_kind = | ListByte diff --git a/kernel/byterun/dune b/kernel/byterun/dune index a2484f79a7..b14ad5c558 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -1,7 +1,7 @@ (library (name byterun) (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]") - (public_name coq.vm) + (public_name coq-core.vm) (foreign_stubs (language c) (names coq_fix_code coq_float64 coq_memory coq_values coq_interp) diff --git a/kernel/dune b/kernel/dune index bd663974da..0bf51f80ec 100644 --- a/kernel/dune +++ b/kernel/dune @@ -1,7 +1,7 @@ (library (name kernel) (synopsis "The Coq Kernel") - (public_name coq.kernel) + (public_name coq-core.kernel) (wrapped false) (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63)) (libraries lib byterun dynlink)) @@ -25,7 +25,7 @@ (action (copy# %{gen-file} %{targets}))) (documentation - (package coq)) + (package coq-core)) ; In dev profile, we check the kernel against a more strict set of ; warnings. diff --git a/lib/control.ml b/lib/control.ml index ea94bda064..5a38022291 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -29,22 +29,32 @@ let check_for_interrupt () = end (** This function does not work on windows, sigh... *) +(* This function assumes it is the only function calling [setitimer] *) let unix_timeout n f x = let open Unix in let timeout_handler _ = raise Timeout in - let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in - let _ = setitimer ITIMER_REAL {it_interval = 0.; it_value = n} in - let restore_timeout () = - let _ = setitimer ITIMER_REAL { it_interval = 0.; it_value = 0. } in - Sys.set_signal Sys.sigalrm psh - in - try - let res = f x in - restore_timeout (); - Some res - with Timeout -> - restore_timeout (); - None + let old_timer = getitimer ITIMER_REAL in + (* Here we assume that the existing timer will also interrupt us. *) + if old_timer.it_value > 0. && old_timer.it_value <= n then Some (f x) else + let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + let old_timer = setitimer ITIMER_REAL {it_interval = 0.; it_value = n} in + let restore_timeout () = + let timer_status = getitimer ITIMER_REAL in + let old_timer_value = old_timer.it_value -. n +. timer_status.it_value in + (* We want to make sure that the parent timer triggers, even if somehow the parent timeout + has already passed. This should not happen, but due to timer imprecision it can happen in practice *) + let old_timer_value = if old_timer.it_value <= 0. then 0. else + (if old_timer_value <= 0. then epsilon_float else old_timer_value) in + let _ = setitimer ITIMER_REAL { old_timer with it_value = old_timer_value } in + Sys.set_signal Sys.sigalrm psh + in + try + let res = f x in + restore_timeout (); + Some res + with Timeout -> + restore_timeout (); + None let windows_timeout n f x = @@ -1,7 +1,7 @@ (library (name lib) (synopsis "Coq's Utility Library [coq-specific]") - (public_name coq.lib) + (public_name coq-core.lib) (wrapped false) (modules_without_implementation xml_datatype) - (libraries coq.clib coq.config)) + (libraries coq-core.clib coq-core.config)) diff --git a/lib/envars.ml b/lib/envars.ml index 1702b5d7a2..823d255f58 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -132,7 +132,9 @@ let guess_coqlib fail = if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude) then Coq_config.coqlib else - fail "cannot guess a path for Coq libraries; please use -coqlib option") + fail "cannot guess a path for Coq libraries; please use -coqlib option \ + or ensure you have installed the package contaning Coq's stdlib (coq-stdlib in OPAM) \ + If you intend to use Coq without a standard library, the -boot -noinit options must be used.") ) let coqlib : string option ref = ref None @@ -205,6 +207,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = let open Printf in fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0"); fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); + fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (if Coq_config.local then coqlib () else coqlib () / "../coq-core/"); fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; diff --git a/library/dune b/library/dune index 344fad5a75..bf90511ead 100644 --- a/library/dune +++ b/library/dune @@ -1,9 +1,9 @@ (library (name library) (synopsis "Coq's Loadable Libraries (vo) Support") - (public_name coq.library) + (public_name coq-core.library) (wrapped false) (libraries kernel)) (documentation - (package coq)) + (package coq-core)) @@ -1,6 +1,6 @@ (install (section man) - (package coq) + (package coq-core) (files coqc.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqchk.1 coqdep.1 coqdoc.1 coq_makefile.1 coq-tex.1 coqwc.1)) (install diff --git a/parsing/dune b/parsing/dune index 8a31434101..17011d10de 100644 --- a/parsing/dune +++ b/parsing/dune @@ -1,7 +1,7 @@ (library (name parsing) - (public_name coq.parsing) + (public_name coq-core.parsing) (wrapped false) - (libraries coq.gramlib interp)) + (libraries coq-core.gramlib interp)) (coq.pp (modules g_prim g_constr)) diff --git a/plugins/btauto/dune b/plugins/btauto/dune index d2f5b65980..f7b3477460 100644 --- a/plugins/btauto/dune +++ b/plugins/btauto/dune @@ -1,7 +1,7 @@ (library (name btauto_plugin) - (public_name coq.plugins.btauto) + (public_name coq-core.plugins.btauto) (synopsis "Coq's btauto plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_btauto)) diff --git a/plugins/cc/dune b/plugins/cc/dune index f7fa3adb56..ee28148c5a 100644 --- a/plugins/cc/dune +++ b/plugins/cc/dune @@ -1,7 +1,7 @@ (library (name cc_plugin) - (public_name coq.plugins.cc) + (public_name coq-core.plugins.cc) (synopsis "Coq's congruence closure plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_congruence)) diff --git a/plugins/derive/dune b/plugins/derive/dune index 1931339471..d382031a58 100644 --- a/plugins/derive/dune +++ b/plugins/derive/dune @@ -1,7 +1,7 @@ (library (name derive_plugin) - (public_name coq.plugins.derive) + (public_name coq-core.plugins.derive) (synopsis "Coq's derive plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_derive)) diff --git a/plugins/extraction/dune b/plugins/extraction/dune index d9d675fe6a..7f2582f84e 100644 --- a/plugins/extraction/dune +++ b/plugins/extraction/dune @@ -1,7 +1,7 @@ (library (name extraction_plugin) - (public_name coq.plugins.extraction) + (public_name coq-core.plugins.extraction) (synopsis "Coq's extraction plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_extraction)) diff --git a/plugins/firstorder/dune b/plugins/firstorder/dune index 1b05452d8f..0299ca802f 100644 --- a/plugins/firstorder/dune +++ b/plugins/firstorder/dune @@ -1,7 +1,7 @@ (library (name ground_plugin) - (public_name coq.plugins.firstorder) + (public_name coq-core.plugins.firstorder) (synopsis "Coq's first order logic solver plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_ground)) diff --git a/plugins/funind/dune b/plugins/funind/dune index e594ffbd02..42377f37f4 100644 --- a/plugins/funind/dune +++ b/plugins/funind/dune @@ -1,7 +1,7 @@ (library (name recdef_plugin) - (public_name coq.plugins.funind) + (public_name coq-core.plugins.funind) (synopsis "Coq's functional induction plugin") - (libraries coq.plugins.extraction)) + (libraries coq-core.plugins.extraction)) (coq.pp (modules g_indfun)) diff --git a/plugins/ltac/dune b/plugins/ltac/dune index 6558ecbfe8..9ec2b10873 100644 --- a/plugins/ltac/dune +++ b/plugins/ltac/dune @@ -1,15 +1,15 @@ (library (name ltac_plugin) - (public_name coq.plugins.ltac) + (public_name coq-core.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) - (libraries coq.stm)) + (libraries coq-core.stm)) (library (name tauto_plugin) - (public_name coq.plugins.tauto) + (public_name coq-core.plugins.tauto) (synopsis "Coq's tauto tactic") (modules tauto) - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6d0e0c36b3..c7bda43465 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -251,10 +251,10 @@ end) = struct (** Folding/unfolding of the tactic constants. *) - let unfold_impl sigma t = + let unfold_impl n sigma t = match EConstr.kind sigma t with | App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) -> - mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b) + mkProd (make_annot n Sorts.Relevant, a, lift 1 b) | _ -> assert false let unfold_all sigma t = @@ -273,16 +273,16 @@ end) = struct | _ -> assert false) | _ -> assert false - let arrow_morphism env evd ta tb a b = + let arrow_morphism env evd n ta tb a b = let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in - if ap && bp then app_poly env evd impl [| a; b |], unfold_impl + if ap && bp then app_poly env evd impl [| a; b |], unfold_impl n else if ap then (* Domain in Prop, CoDomain in Type *) - (app_poly env evd arrow [| a; b |]), unfold_impl + (app_poly env evd arrow [| a; b |]), unfold_impl n (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (make_annot n Sorts.Relevant, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) - (app_poly env evd arrow [| a; b |]), unfold_impl + (app_poly env evd arrow [| a; b |]), unfold_impl n let rec decomp_pointwise sigma n c = if Int.equal n 0 then c @@ -1079,7 +1079,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let arr = if prop then PropGlobal.arrow_morphism else TypeGlobal.arrow_morphism in - let (evars', mor), unfold = arr env evars tx tb x b in + let (evars', mor), unfold = arr env evars n.binder_name tx tb x b in let state, res = aux { state ; env ; unfresh ; term1 = mor ; ty1 = ty ; cstr = (prop,cstr) ; evars = evars' } in diff --git a/plugins/micromega/dune b/plugins/micromega/dune index 204125ab56..41f894bce3 100644 --- a/plugins/micromega/dune +++ b/plugins/micromega/dune @@ -1,24 +1,24 @@ (library (name micromega_plugin) - (public_name coq.plugins.micromega) + (public_name coq-core.plugins.micromega) ; be careful not to link the executable to the plugin! (modules (:standard \ csdpcert g_zify zify)) (synopsis "Coq's micromega plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (executable (name csdpcert) (public_name csdpcert) - (package coq) + (package coq-core) (modules csdpcert) (flags :standard -open Micromega_plugin) - (libraries coq.plugins.micromega)) + (libraries coq-core.plugins.micromega)) (library (name zify_plugin) - (public_name coq.plugins.zify) + (public_name coq-core.plugins.zify) (modules g_zify zify) (synopsis "Coq's zify plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_micromega g_zify)) diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune index 3b67ab3429..2aaeec2665 100644 --- a/plugins/nsatz/dune +++ b/plugins/nsatz/dune @@ -1,7 +1,7 @@ (library (name nsatz_plugin) - (public_name coq.plugins.nsatz) + (public_name coq-core.plugins.nsatz) (synopsis "Coq's nsatz solver plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_nsatz)) diff --git a/plugins/omega/dune b/plugins/omega/dune index 0db71ed6fb..a3c9342322 100644 --- a/plugins/omega/dune +++ b/plugins/omega/dune @@ -1,7 +1,7 @@ (library (name omega_plugin) - (public_name coq.plugins.omega) + (public_name coq-core.plugins.omega) (synopsis "Coq's omega plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_omega)) diff --git a/plugins/ring/dune b/plugins/ring/dune index 080d8c672e..40f310831a 100644 --- a/plugins/ring/dune +++ b/plugins/ring/dune @@ -1,7 +1,7 @@ (library (name ring_plugin) - (public_name coq.plugins.ring) + (public_name coq-core.plugins.ring) (synopsis "Coq's ring plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_ring)) diff --git a/plugins/rtauto/dune b/plugins/rtauto/dune index 43efa0eca5..a13f063550 100644 --- a/plugins/rtauto/dune +++ b/plugins/rtauto/dune @@ -1,7 +1,7 @@ (library (name rtauto_plugin) - (public_name coq.plugins.rtauto) + (public_name coq-core.plugins.rtauto) (synopsis "Coq's rtauto plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_rtauto)) diff --git a/plugins/ssr/dune b/plugins/ssr/dune index a117d09a16..4c28776bb7 100644 --- a/plugins/ssr/dune +++ b/plugins/ssr/dune @@ -1,9 +1,9 @@ (library (name ssreflect_plugin) - (public_name coq.plugins.ssreflect) + (public_name coq-core.plugins.ssreflect) (synopsis "Coq's ssreflect plugin") (modules_without_implementation ssrast) (flags :standard -open Gramlib) - (libraries coq.plugins.ssrmatching)) + (libraries coq-core.plugins.ssrmatching)) (coq.pp (modules ssrvernac ssrparser)) diff --git a/plugins/ssrmatching/dune b/plugins/ssrmatching/dune index 629d723816..efaa09c939 100644 --- a/plugins/ssrmatching/dune +++ b/plugins/ssrmatching/dune @@ -1,7 +1,7 @@ (library (name ssrmatching_plugin) - (public_name coq.plugins.ssrmatching) + (public_name coq-core.plugins.ssrmatching) (synopsis "Coq ssrmatching plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_ssrmatching)) diff --git a/plugins/ssrsearch/dune b/plugins/ssrsearch/dune index 2851835eae..a38bec496f 100644 --- a/plugins/ssrsearch/dune +++ b/plugins/ssrsearch/dune @@ -1,7 +1,7 @@ (library (name ssrsearch_plugin) - (public_name coq.plugins.ssrsearch) + (public_name coq-core.plugins.ssrsearch) (synopsis "Deprecated Search command from SSReflect") - (libraries coq.plugins.ssreflect)) + (libraries coq-core.plugins.ssreflect)) (coq.pp (modules g_search)) diff --git a/plugins/syntax/dune b/plugins/syntax/dune index ba53a439a0..b00242be1a 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -1,15 +1,15 @@ (library (name number_string_notation_plugin) - (public_name coq.plugins.number_string_notation) + (public_name coq-core.plugins.number_string_notation) (synopsis "Coq number and string notation plugin") (modules g_number_string string_notation number) - (libraries coq.vernac)) + (libraries coq-core.vernac)) (library (name float_syntax_plugin) - (public_name coq.plugins.float_syntax) + (public_name coq-core.plugins.float_syntax) (synopsis "Coq syntax plugin: float") (modules float_syntax) - (libraries coq.vernac)) + (libraries coq-core.vernac)) (coq.pp (modules g_number_string)) diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml index 80c11dc0d4..551e2bac5d 100644 --- a/plugins/syntax/number.ml +++ b/plugins/syntax/number.ml @@ -131,13 +131,6 @@ let type_error_of g ty = str " to Number.int or (option Number.int)." ++ fnl () ++ str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).") -let warn_deprecated_decimal = - CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" - (fun () -> - strbrk "Deprecated Number Notation for Decimal.uint, \ - Decimal.int or Decimal.decimal. Use Number.uint, \ - Number.int or Number.number respectively.") - let error_params ind = CErrors.user_err (str "Wrong number of parameters for inductive" ++ spc () @@ -456,12 +449,6 @@ let vernac_number_notation local ty f g opts scope = | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option | _ -> match z_pos_ty with | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct @@ -484,12 +471,6 @@ let vernac_number_notation local ty f g opts scope = | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option | _ -> match z_pos_ty with | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct @@ -500,11 +481,6 @@ let vernac_number_notation local ty f g opts scope = | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty (opt cint63)) -> Int63 pos_neg_int63_ty, Option | _ -> type_error_of g ty in - (match to_kind, of_kind with - | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _ - | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> - warn_deprecated_decimal () - | _ -> ()); let to_post, pt_required, pt_refs = match tyc_params with | TargetPrim path -> [||], path, [Coqlib.lib_ref "num.int63.wrap_int"] | TargetInd (tyc, params) -> diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index 8ddc576d83..ac89dfd747 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -156,8 +156,6 @@ let cl_fun_index = fst(class_info CL_FUN) let cl_sort_index = fst(class_info CL_SORT) -(* coercion_info : coe_typ -> coe_info_typ *) - let coercion_info coe = CoeTypMap.find coe !coercion_tab let coercion_exists coe = CoeTypMap.mem coe !coercion_tab diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index 31600dd17f..073500b155 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -92,6 +92,8 @@ val declare_coercion : env -> evar_map -> coercion -> unit (** {6 Access to coercions infos } *) val coercion_exists : coe_typ -> bool +val coercion_info : coe_typ -> coe_info_typ + (** {6 Lookup functions for coercion paths } *) (** @raise Not_found in the following functions when no path exists *) diff --git a/pretyping/dune b/pretyping/dune index 14bce92de1..d9b5609bd4 100644 --- a/pretyping/dune +++ b/pretyping/dune @@ -1,6 +1,6 @@ (library (name pretyping) (synopsis "Coq's Type Inference Component (Pretyper)") - (public_name coq.pretyping) + (public_name coq-core.pretyping) (wrapped false) (libraries engine)) diff --git a/printing/dune b/printing/dune index 3392342165..a24a7535eb 100644 --- a/printing/dune +++ b/printing/dune @@ -1,6 +1,6 @@ (library (name printing) (synopsis "Coq's Term Pretty Printing Library") - (public_name coq.printing) + (public_name coq-core.printing) (wrapped false) (libraries parsing proofs)) diff --git a/proofs/dune b/proofs/dune index 36e9799998..f8e7661997 100644 --- a/proofs/dune +++ b/proofs/dune @@ -1,6 +1,6 @@ (library (name proofs) (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure") - (public_name coq.proofs) + (public_name coq-core.proofs) (wrapped false) (libraries pretyping)) diff --git a/proofs/refine.ml b/proofs/refine.ml index ac410a958f..ce04c35e11 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -129,7 +129,6 @@ let solve_constraints = tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Unsafe.tclEVARSADVANCE sigma - with e -> - (* XXX this is absorbing anomalies? *) + with e when CErrors.noncritical e -> let info = Exninfo.reify () in tclZERO ~info e @@ -1,6 +1,6 @@ (library (name stm) (synopsis "Coq's Document Manager and Proof Checking Scheduler") - (public_name coq.stm) + (public_name coq-core.stm) (wrapped false) (libraries sysinit)) diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml index 8635345e00..95ae5da3de 100644 --- a/sysinit/coqloadpath.ml +++ b/sysinit/coqloadpath.ml @@ -44,8 +44,18 @@ let init_load_path ~coqlib = let coq_path = Names.DirPath.make [Libnames.coq_root] in (* ML includes *) - let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in - + let unix_path = + (* Usually lib/coq-stdlib/../plugins ; this kind of hacks with the + ML path should go away once we use ocamlfind to load plugins *) + CPath.choose_existing + [ CPath.make [ coqlib ; "plugins" ] + ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] + ] |> function + | None -> + CErrors.user_err (Pp.str "Cannot find plugins directory") + | Some f -> (f :> string) + in + let plugins_dirs = System.all_subdirs ~unix_path |> List.map fst in let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in let misc_ml, misc_vo = diff --git a/sysinit/dune b/sysinit/dune index 04b46fb2a2..f882f987ff 100644 --- a/sysinit/dune +++ b/sysinit/dune @@ -1,7 +1,6 @@ (library (name sysinit) - (public_name coq.sysinit) + (public_name coq-core.sysinit) (synopsis "Coq's initialization") (wrapped false) - (libraries coq.vernac) - ) + (libraries coq-core.vernac)) diff --git a/tactics/dune b/tactics/dune index 908dde5253..29378f52d1 100644 --- a/tactics/dune +++ b/tactics/dune @@ -1,6 +1,6 @@ (library (name tactics) (synopsis "Coq's Core Tactics [ML implementation]") - (public_name coq.tactics) + (public_name coq-core.tactics) (wrapped false) (libraries printing)) diff --git a/tactics/hints.ml b/tactics/hints.ml index 058602acfd..5e9c3baeb1 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1019,18 +1019,6 @@ let remove_hint dbname grs = let db' = Hint_db.remove_list env grs db in searchtable_add (dbname, db') -type hint_action = - | CreateDB of bool * TransparentState.t - | AddTransparency of { - superglobal : bool; - grefs : evaluable_global_reference hints_transparency_target; - state : bool; - } - | AddHints of { superglobal : bool; hints : hint_entry list } - | RemoveHints of { superglobal : bool; hints : GlobRef.t list } - | AddCut of { superglobal : bool; paths : hints_path } - | AddMode of { superglobal : bool; gref : GlobRef.t; mode : hint_mode array } - let add_cut dbname path = let db = get_db dbname in let db' = Hint_db.add_cut path db in @@ -1041,30 +1029,72 @@ let add_mode dbname l m = let db' = Hint_db.add_mode l m db in searchtable_add (dbname, db') +type db_obj = { + db_local : bool; + db_name : string; + db_use_dn : bool; + db_ts : TransparentState.t; +} + +let cache_db (_, {db_name=name; db_use_dn=b; db_ts=ts}) = + searchtable_add (name, Hint_db.empty ~name ts b) + +let load_db _ x = cache_db x + +let classify_db db = if db.db_local then Dispose else Substitute db + +let inDB : db_obj -> obj = + declare_object {(default_object "AUTOHINT_DB") with + cache_function = cache_db; + load_function = load_db; + subst_function = (fun (_,x) -> x); + classify_function = classify_db; } + +let create_hint_db l n ts b = + let hint = {db_local=l; db_name=n; db_use_dn=b; db_ts=ts} in + Lib.add_anonymous_leaf (inDB hint) + +type hint_action = + | AddTransparency of { + grefs : evaluable_global_reference hints_transparency_target; + state : bool; + } + | AddHints of hint_entry list + | RemoveHints of GlobRef.t list + | AddCut of hints_path + | AddMode of { gref : GlobRef.t; mode : hint_mode array } + +type hint_locality = Local | Export | SuperGlobal + type hint_obj = { - hint_local : bool; + hint_local : hint_locality; hint_name : string; hint_action : hint_action; } +let superglobal h = match h.hint_local with + | SuperGlobal -> true + | Local | Export -> false + let load_autohint _ (kn, h) = let name = h.hint_name in + let superglobal = superglobal h in match h.hint_action with - | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b) - | AddTransparency { superglobal; grefs; state } -> + | AddTransparency { grefs; state } -> if superglobal then add_transparency name grefs state - | AddHints { superglobal; hints } -> + | AddHints hints -> if superglobal then add_hint name hints - | RemoveHints { superglobal; hints } -> + | RemoveHints hints -> if superglobal then remove_hint name hints - | AddCut { superglobal; paths } -> + | AddCut paths -> if superglobal then add_cut name paths - | AddMode { superglobal; gref; mode } -> + | AddMode { gref; mode } -> if superglobal then add_mode name gref mode let open_autohint i (kn, h) = + let superglobal = superglobal h in if Int.equal i 1 then match h.hint_action with - | AddHints { superglobal; hints } -> + | AddHints hints -> let () = if not superglobal then (* Import-bound hints must be declared when not imported yet *) @@ -1073,15 +1103,14 @@ let open_autohint i (kn, h) = in let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in List.iter add hints - | AddCut { superglobal; paths } -> + | AddCut paths -> if not superglobal then add_cut h.hint_name paths - | AddTransparency { superglobal; grefs; state } -> + | AddTransparency { grefs; state } -> if not superglobal then add_transparency h.hint_name grefs state - | RemoveHints { superglobal; hints } -> + | RemoveHints hints -> if not superglobal then remove_hint h.hint_name hints - | AddMode { superglobal; gref; mode } -> + | AddMode { gref; mode } -> if not superglobal then add_mode h.hint_name gref mode - | CreateDB _ -> () let cache_autohint (kn, obj) = load_autohint 1 (kn, obj); open_autohint 1 (kn, obj) @@ -1137,8 +1166,7 @@ let subst_autohint (subst, obj) = if k' == k && data' == data then hint else (k',data') in let action = match obj.hint_action with - | CreateDB _ -> obj.hint_action - | AddTransparency { superglobal; grefs = target; state = b } -> + | AddTransparency { grefs = target; state = b } -> let target' = match target with | HintsVariables -> target @@ -1148,26 +1176,28 @@ let subst_autohint (subst, obj) = if grs == grs' then target else HintsReferences grs' in - if target' == target then obj.hint_action else AddTransparency { superglobal; grefs = target'; state = b } - | AddHints { superglobal; hints } -> + if target' == target then obj.hint_action else AddTransparency { grefs = target'; state = b } + | AddHints hints -> let hints' = List.Smart.map subst_hint hints in - if hints' == hints then obj.hint_action else AddHints { superglobal; hints = hints' } - | RemoveHints { superglobal; hints = grs } -> + if hints' == hints then obj.hint_action else AddHints hints' + | RemoveHints grs -> let grs' = List.Smart.map (subst_global_reference subst) grs in - if grs == grs' then obj.hint_action else RemoveHints { superglobal; hints = grs' } - | AddCut { superglobal; paths = path } -> + if grs == grs' then obj.hint_action else RemoveHints grs' + | AddCut path -> let path' = subst_hints_path subst path in - if path' == path then obj.hint_action else AddCut { superglobal; paths = path' } - | AddMode { superglobal; gref = l; mode = m } -> + if path' == path then obj.hint_action else AddCut path' + | AddMode { gref = l; mode = m } -> let l' = subst_global_reference subst l in - if l' == l then obj.hint_action else AddMode { superglobal; gref = l'; mode = m } + if l' == l then obj.hint_action else AddMode { gref = l'; mode = m } in if action == obj.hint_action then obj else { obj with hint_action = action } let classify_autohint obj = match obj.hint_action with - | AddHints { hints = [] } -> Dispose - | _ -> if obj.hint_local then Dispose else Substitute obj + | AddHints [] -> Dispose + | _ -> match obj.hint_local with + | Local -> Dispose + | Export | SuperGlobal -> Substitute obj let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with @@ -1177,16 +1207,12 @@ let inAutoHint : hint_obj -> obj = subst_function = subst_autohint; classify_function = classify_autohint; } -let make_hint ?(local = false) name action = { +let make_hint ~local name action = { hint_local = local; hint_name = name; hint_action = action; } -let create_hint_db l n st b = - let hint = make_hint ~local:l n (CreateDB (b, st)) in - Lib.add_anonymous_leaf (inAutoHint hint) - let warn_deprecated_hint_without_locality = CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated" (fun () -> strbrk "The default value for hint locality is currently \ @@ -1210,16 +1236,16 @@ let check_hint_locality = let open Goptions in function | OptLocal -> () let interp_locality = function -| Goptions.OptDefault | Goptions.OptGlobal -> false, true -| Goptions.OptExport -> false, false -| Goptions.OptLocal -> true, false +| Goptions.OptDefault | Goptions.OptGlobal -> SuperGlobal +| Goptions.OptExport -> Export +| Goptions.OptLocal -> Local let remove_hints ~locality dbnames grs = - let local, superglobal = interp_locality locality in + let local = interp_locality locality in let dbnames = if List.is_empty dbnames then ["core"] else dbnames in List.iter (fun dbname -> - let hint = make_hint ~local dbname (RemoveHints { superglobal; hints = grs }) in + let hint = make_hint ~local dbname (RemoveHints grs) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1227,7 +1253,7 @@ let remove_hints ~locality dbnames grs = (* The "Hint" vernacular command *) (**************************************************************************) -let add_resolves env sigma clist ~local ~superglobal dbnames = +let add_resolves env sigma clist ~local dbnames = List.iter (fun dbname -> let r = @@ -1254,56 +1280,56 @@ let add_resolves env sigma clist ~local ~superglobal dbnames = | _ -> () in let () = if not !Flags.quiet then List.iter check r in - let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in + let hint = make_hint ~local dbname (AddHints r) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_unfolds l ~local ~superglobal dbnames = +let add_unfolds l ~local dbnames = List.iter (fun dbname -> - let hint = make_hint ~local dbname (AddHints { superglobal; hints = List.map make_unfold l }) in + let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_cuts l ~local ~superglobal dbnames = +let add_cuts l ~local dbnames = List.iter (fun dbname -> - let hint = make_hint ~local dbname (AddCut { superglobal; paths = l }) in + let hint = make_hint ~local dbname (AddCut l) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_mode l m ~local ~superglobal dbnames = +let add_mode l m ~local dbnames = List.iter (fun dbname -> let m' = make_mode l m in - let hint = make_hint ~local dbname (AddMode { superglobal; gref = l; mode = m' }) in + let hint = make_hint ~local dbname (AddMode { gref = l; mode = m' }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_transparency l b ~local ~superglobal dbnames = +let add_transparency l b ~local dbnames = List.iter (fun dbname -> - let hint = make_hint ~local dbname (AddTransparency { superglobal; grefs = l; state = b }) in + let hint = make_hint ~local dbname (AddTransparency { grefs = l; state = b }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_extern info tacast ~local ~superglobal dbname = +let add_extern info tacast ~local dbname = let pat = match info.hint_pattern with | None -> None | Some (_, pat) -> Some pat in let hint = make_hint ~local dbname - (AddHints { superglobal; hints = [make_extern (Option.get info.hint_priority) pat tacast] }) in + (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in Lib.add_anonymous_leaf (inAutoHint hint) -let add_externs info tacast ~local ~superglobal dbnames = - List.iter (add_extern info tacast ~local ~superglobal) dbnames +let add_externs info tacast ~local dbnames = + List.iter (add_extern info tacast ~local) dbnames -let add_trivials env sigma l ~local ~superglobal dbnames = +let add_trivials env sigma l ~local dbnames = List.iter (fun dbname -> let l = List.map (fun (name, c) -> make_trivial env sigma ~name c) l in - let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in + let hint = make_hint ~local dbname (AddHints l) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1360,22 +1386,22 @@ let prepare_hint check env init (sigma,c) = (c', diff) let add_hints ~locality dbnames h = - let local, superglobal = interp_locality locality in + let local = interp_locality locality in if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); assert (not (List.is_empty dbnames)); let env = Global.env() in let sigma = Evd.from_env env in match h with - | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames - | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames - | HintsCutEntry lhints -> add_cuts lhints ~local ~superglobal dbnames - | HintsModeEntry (l,m) -> add_mode l m ~local ~superglobal dbnames - | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames + | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local dbnames + | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local dbnames + | HintsCutEntry lhints -> add_cuts lhints ~local dbnames + | HintsModeEntry (l,m) -> add_mode l m ~local dbnames + | HintsUnfoldEntry lhints -> add_unfolds lhints ~local dbnames | HintsTransparencyEntry (lhints, b) -> - add_transparency lhints b ~local ~superglobal dbnames + add_transparency lhints b ~local dbnames | HintsExternEntry (info, tacexp) -> - add_externs info tacexp ~local ~superglobal dbnames + add_externs info tacexp ~local dbnames let hint_globref gr = IsGlobRef gr diff --git a/test-suite/Makefile b/test-suite/Makefile index 245c717d42..2a2f62e23f 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -46,7 +46,11 @@ BIN := $(ROOT)/bin/ COQLIB?= ifeq ($(COQLIB),) + ifeq ($(LOCAL),true) COQLIB := $(shell ocaml ocaml_pwd.ml ..) + else + COQLIB := $(shell ocaml ocaml_pwd.ml $(COQLIBINSTALL)) + endif endif endif # exists ../_build export COQLIB @@ -320,7 +324,7 @@ unit-tests: $(UNIT_LOGFILES) # Build executable, run it to generate log file unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,ounit2 \ + $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq-core.toplevel,ounit2 \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test diff --git a/test-suite/bugs/closed/bug_12011.v b/test-suite/bugs/closed/bug_12011.v new file mode 100644 index 0000000000..f149b4e8ae --- /dev/null +++ b/test-suite/bugs/closed/bug_12011.v @@ -0,0 +1,21 @@ +From Coq Require Import Setoid ssreflect. + +Lemma test A (R : relation A) `{Equivalence _ R} (x y z : A) : + R x y -> R y z -> R x z. +Proof. + intros Hxy Hyz. + rewrite -Hxy in Hyz. + exact Hyz. +Qed. + + + +Axiom envs_lookup_delete : bool. +Axiom envs_lookup_delete_Some : envs_lookup_delete = true <-> False. + +Goal envs_lookup_delete = true -> False. +Proof. +intros Hlookup. +rewrite envs_lookup_delete_Some in Hlookup *. (* <- used to revert Hlookup *) +exact Hlookup. +Qed. diff --git a/test-suite/bugs/closed/bug_13586.v b/test-suite/bugs/closed/bug_13586.v new file mode 100644 index 0000000000..6a739c364a --- /dev/null +++ b/test-suite/bugs/closed/bug_13586.v @@ -0,0 +1,6 @@ +Goal True. +Fail timeout 2 ((timeout 1 repeat cut True) || (repeat cut True)). +Fail Timeout 2 ((timeout 1 repeat cut True) || (repeat cut True)). +Fail timeout 1 ((timeout 2 repeat cut True) || idtac "fail"). +auto. +Qed. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in index 47d0e09e1a..258eb04271 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in @@ -744,7 +744,7 @@ CONTRIBUTING.md CREDITS INSTALL.md LICENSE -META.coq.in +META.coq-core.in Makefile Makefile.build Makefile.checker @@ -5626,4 +5626,4 @@ ValueError: too many values to unpack Makefile.ci:90: recipe for target 'ci-metacoq' failed make: *** [ci-metacoq] Error 1 section_end:1598965182:build_script
[0Ksection_start:1598965182:after_script
[0Ksection_end:1598965184:after_script
[0Ksection_start:1598965184:upload_artifacts_on_failure
[0Ksection_end:1598965189:upload_artifacts_on_failure
[0K[31;1mERROR: Job failed: exit code 1 -[0;m
\ No newline at end of file +[0;m diff --git a/test-suite/dune b/test-suite/dune index 1864153021..09597fc864 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -35,7 +35,8 @@ ; For the changelog test ../config/coq_config.py (source_tree doc/changelog) - (package coq) + (package coq-core) + (package coq-stdlib) ; For fake_ide (package coqide-server) (source_tree .)) diff --git a/test-suite/ltac2/printf.v b/test-suite/ltac2/printf.v new file mode 100644 index 0000000000..f96a01a9c9 --- /dev/null +++ b/test-suite/ltac2/printf.v @@ -0,0 +1,31 @@ +Require Import Ltac2.Ltac2. +Require Import Ltac2.Printf. + +(* Check that the arguments have type unit *) +Ltac2 ignore (x : unit) := (). + +Ltac2 dummy (_ : unit) (_ : int) := Message.of_string "dummy". + +(** Simple test for all specifications *) + +Ltac2 Eval ignore (printf "%i" 42). +Ltac2 Eval ignore (printf "%s" "abc"). +Ltac2 Eval ignore (printf "%I" @Foo). +Ltac2 Eval ignore (printf "%t" '(1 + 1 = 0)). +Ltac2 Eval ignore (printf "%%"). +Ltac2 Eval ignore (printf "%a" dummy 18). + +(** More complex tests *) + +Ltac2 Eval ignore (printf "%I foo%a bar %s" @ok dummy 18 "yes"). + +Ltac2 Eval Message.print (fprintf "%I foo%a bar %s" @ok dummy 18 "yes"). + +(** Failure tests *) + +Fail Ltac2 Eval printf "%i" "foo". +Fail Ltac2 Eval printf "%s" 0. +Fail Ltac2 Eval printf "%I" "foo". +Fail Ltac2 Eval printf "%t" "foo". +Fail Ltac2 Eval printf "%a" (fun _ _ => ()). +Fail Ltac2 Eval printf "%a" (fun _ i => Message.of_int i) "foo". diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh index 667d11f89e..6f7b11c8f1 100755 --- a/test-suite/misc/coq_environment.sh +++ b/test-suite/misc/coq_environment.sh @@ -16,7 +16,7 @@ EOT cp $BIN/coqc . cp $BIN/coq_makefile . mkdir -p overridden/tools/ -cp $COQLIB/tools/CoqMakefile.in overridden/tools/ +cp $COQLIB/tools/CoqMakefile.in overridden/tools/ || cp $COQLIB/../coq-core/tools/CoqMakefile.in overridden/tools/ unset COQLIB N=`./coqc -config | grep COQLIB | grep /overridden | wc -l` diff --git a/theories/dune b/theories/dune index 90e9522b7b..1cd3d8c119 100644 --- a/theories/dune +++ b/theories/dune @@ -1,6 +1,6 @@ (coq.theory (name Coq) - (package coq) + (package coq-stdlib) (synopsis "Coq's Standard Library") (flags -q) ; (mode native) @@ -8,29 +8,29 @@ ; (per_file ; (Init/*.v -> -boot)) (libraries - coq.plugins.ltac - coq.plugins.tauto + coq-core.plugins.ltac + coq-core.plugins.tauto - coq.plugins.cc - coq.plugins.firstorder + coq-core.plugins.cc + coq-core.plugins.firstorder - coq.plugins.number_string_notation - coq.plugins.float_syntax + coq-core.plugins.number_string_notation + coq-core.plugins.float_syntax - coq.plugins.btauto - coq.plugins.rtauto + coq-core.plugins.btauto + coq-core.plugins.rtauto - coq.plugins.ring - coq.plugins.nsatz - coq.plugins.omega + coq-core.plugins.ring + coq-core.plugins.nsatz + coq-core.plugins.omega - coq.plugins.zify - coq.plugins.micromega + coq-core.plugins.zify + coq-core.plugins.micromega - coq.plugins.funind + coq-core.plugins.funind - coq.plugins.ssreflect - coq.plugins.ssrsearch - coq.plugins.derive)) + coq-core.plugins.ssreflect + coq-core.plugins.ssrsearch + coq-core.plugins.derive)) (include_subdirs qualified) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0ebb97d0bf..f2f2111fae 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -37,6 +37,7 @@ COQLIBS_NOML := $(COQMF_COQLIBS_NOML) CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS) LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) +COQCORELIB := $(COQMF_COQCORELIB) DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) CAMLFLAGS := $(COQMF_CAMLFLAGS) @@ -97,9 +98,9 @@ COQMKFILE ?= "$(COQBIN)coq_makefile" OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" # Timing scripts -COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" +COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" BEFORE ?= AFTER ?= @@ -220,7 +221,7 @@ COQDOCLIBS?=$(COQLIBS_NOML) COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQCORELIB)/$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) # ocamldoc fails with unknown argument otherwise @@ -822,6 +823,7 @@ printenv:: $(warning write extensions in @LOCAL_FILE@ or include @CONF_FILE@) @echo 'LOCAL = $(LOCAL)' @echo 'COQLIB = $(COQLIB)' + @echo 'COQCORELIB = $(COQCORELIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @@ -840,12 +842,12 @@ printenv:: .merlin: $(SHOW)'FILL .merlin' $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin - $(HIDE)echo 'B $(COQLIB)' >> .merlin - $(HIDE)echo 'S $(COQLIB)' >> .merlin + $(HIDE)echo 'B $(COQCORELIB)' >> .merlin + $(HIDE)echo 'S $(COQCORELIB)' >> .merlin $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'B $(COQLIB)$(d)' >> .merlin;) + echo 'B $(COQCORELIB)$(d)' >> .merlin;) $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'S $(COQLIB)$(d)' >> .merlin;) + echo 'S $(COQCORELIB)$(d)' >> .merlin;) $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 07550b67e3..cddb840693 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -125,8 +125,17 @@ let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" let generate_makefile oc conf_file local_file dep_file args project = let coqlib = Envars.coqlib () in let makefile_template = - let template = Filename.concat "tools" "CoqMakefile.in" in - Filename.concat coqlib template in + CPath.choose_existing + [ CPath.make [ coqlib; "tools"; "CoqMakefile.in" ] + ; CPath.make [ coqlib; ".."; "coq-core"; "tools"; "CoqMakefile.in" ] + ] + in + let makefile_template = match makefile_template with + | None -> + Format.eprintf "Error: cannot find CoqMakefile.in"; + exit 1 + | Some v -> (v :> string) + in let s = read_whole_file makefile_template in let s = List.fold_left (* We use global_substitute to avoid running into backslash issues due to \1 etc. *) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2177da0c75..f1dbac889b 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -97,8 +97,16 @@ let coqdep () = if not !option_boot then begin Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg)); let coqlib = Envars.coqlib () in + let coq_plugins_dir = CPath.choose_existing + [ CPath.make [ coqlib; "plugins" ] + ; CPath.make [ coqlib; ".."; "coq-core"; "plugins" ] + ] |> function + | None -> + CErrors.user_err (Pp.str "coqdep: cannot find plugins directory\n"); + | Some f -> (f :> string) + in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; - add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; + add_rec_dir_import add_coqlib_known (coq_plugins_dir) ["Coq"]; let user = coqlib//"user-contrib" in if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user []; List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune index e3c792f277..cc888a959f 100644 --- a/tools/coqdoc/dune +++ b/tools/coqdoc/dune @@ -1,6 +1,6 @@ (install (section lib) - (package coq) + (package coq-core) (files (coqdoc.css as tools/coqdoc/coqdoc.css) (coqdoc.sty as tools/coqdoc/coqdoc.sty))) @@ -8,7 +8,7 @@ (executable (name main) (public_name coqdoc) - (package coq) - (libraries str coq.config coq.clib)) + (package coq-core) + (libraries str coq-core.config coq-core.clib)) (ocamllex cpretty) diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index b8d5032373..c95d1ee7db 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -471,9 +471,17 @@ let index_module = function | Latex_file _ -> () let copy_style_file file = - let src = - List.fold_left - Filename.concat !Cdglobals.coqlib_path ["tools";"coqdoc";file] in + (* We give preference to coqlib in case it is overriden *) + let src_dir = CPath.choose_existing + [ CPath.make [ !Cdglobals.coqlib_path; "tools"; "coqdoc" ] + ; CPath.make [ !Cdglobals.coqlib_path; ".."; "coq-core"; "tools"; "coqdoc" ] + ] |> function + | None -> + eprintf "coqdoc: cannot find coqdoc style files\n"; + exit 1 + | Some f -> f + in + let src = (CPath.relative src_dir file :> string) in let dst = coqdoc_out file in if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src diff --git a/tools/dune b/tools/dune index d591bb0c37..703342b15c 100644 --- a/tools/dune +++ b/tools/dune @@ -1,6 +1,6 @@ (install (section lib) - (package coq) + (package coq-core) (files (CoqMakefile.in as tools/CoqMakefile.in) (TimeFileMaker.py as tools/TimeFileMaker.py) @@ -11,30 +11,30 @@ (executable (name coq_makefile) (public_name coq_makefile) - (package coq) + (package coq-core) (modules coq_makefile) - (libraries coq.lib)) + (libraries coq-core.lib)) (executable (name coqworkmgr) (public_name coqworkmgr) - (package coq) + (package coq-core) (modules coqworkmgr) - (libraries coq.stm)) + (libraries coq-core.stm)) (executable (name coqdep) (public_name coqdep) - (package coq) + (package coq-core) (modules coqdep_lexer coqdep_common coqdep) - (libraries coq.lib)) + (libraries coq-core.lib)) ; Bare-bones mllib/mlpack parser (executable (name ocamllibdep) (public_name ocamllibdep) (modules ocamllibdep) - (package coq) + (package coq-core) (libraries unix)) (ocamllex coqdep_lexer ocamllibdep) @@ -42,7 +42,7 @@ (executable (name coqwc) (public_name coqwc) - (package coq) + (package coq-core) (modules coqwc) (libraries)) @@ -51,6 +51,6 @@ (executables (names coq_tex) (public_names coq-tex) - (package coq) + (package coq-core) (modules coq_tex) (libraries str)) diff --git a/topbin/dune b/topbin/dune index 46052c81e5..5fcb3415f0 100644 --- a/topbin/dune +++ b/topbin/dune @@ -1,31 +1,31 @@ (install (section bin) - (package coq) + (package coq-core) (files (coqtop_bin.exe as coqtop))) (executable (name coqtop_bin) (public_name coqtop.opt) - (package coq) + (package coq-core) (modules coqtop_bin) - (libraries coq.toplevel) + (libraries coq-core.toplevel) (link_flags -linkall)) (executable (name coqtop_byte_bin) (public_name coqtop.byte) - (package coq) + (package coq-core) (modules coqtop_byte_bin) - (libraries compiler-libs.toplevel coq.toplevel) + (libraries compiler-libs.toplevel coq-core.toplevel) (modes byte) (link_flags -linkall)) (executable (name coqc_bin) (public_name coqc) - (package coq) + (package coq-core) (modules coqc_bin) - (libraries coq.toplevel) + (libraries coq-core.toplevel) (modes native byte) ; Adding -ccopt -flto to links options could be interesting, however, ; it doesn't work on Windows @@ -33,16 +33,16 @@ (install (section bin) - (package coq) + (package coq-core) (files (coqc_bin.bc as coqc.byte))) ; Workers (executables (names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin) (public_names coqqueryworker.opt coqtacticworker.opt coqproofworker.opt) - (package coq) + (package coq-core) (modules :standard \ coqtop_byte_bin coqtop_bin coqc_bin) - (libraries coq.toplevel) + (libraries coq-core.toplevel) (link_flags -linkall)) ; Workers installed targets diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 6460378edc..4faecd2e62 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -480,6 +480,11 @@ let drop_args = ref None (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path ~coqlib = + let coqlib : string = + if Sys.file_exists (CPath.make [coqlib; "plugins"] :> string) + then coqlib + else (CPath.make [ coqlib ; ".."; "coq-core" ] :> string) + in let add_subdir dl = Mltop.add_ml_dir (Filename.concat coqlib dl) in List.iter add_subdir ("dev" :: Coq_config.all_src_dirs) diff --git a/toplevel/dune b/toplevel/dune index 98f4ba2edf..9d5a08dde7 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -1,9 +1,9 @@ (library (name toplevel) - (public_name coq.toplevel) + (public_name coq-core.toplevel) (synopsis "Coq's Interactive Shell [terminal-based]") (wrapped false) - (libraries coq.stm)) + (libraries coq-core.stm)) ; Interp provides the `zarith` library to plugins, we could also use ; -linkall in the plugins file, to be discussed. diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index a4f6d497df..097a0ca25f 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -35,6 +35,7 @@ Ltac2 Type preterm. Ltac2 Type binder. Ltac2 Type message. +Ltac2 Type ('a, 'b, 'c, 'd) format. Ltac2 Type exn := [ .. ]. Ltac2 Type 'a array. diff --git a/user-contrib/Ltac2/Ltac2.v b/user-contrib/Ltac2/Ltac2.v index d3bf3c10ea..ccfc7e4a70 100644 --- a/user-contrib/Ltac2/Ltac2.v +++ b/user-contrib/Ltac2/Ltac2.v @@ -22,5 +22,6 @@ Require Ltac2.Fresh. Require Ltac2.Pattern. Require Ltac2.Std. Require Ltac2.Env. +Require Ltac2.Printf. Require Ltac2.Ltac1. Require Export Ltac2.Notations. diff --git a/user-contrib/Ltac2/Message.v b/user-contrib/Ltac2/Message.v index 4a4d1d815c..39d39562cf 100644 --- a/user-contrib/Ltac2/Message.v +++ b/user-contrib/Ltac2/Message.v @@ -25,3 +25,32 @@ Ltac2 @ external of_exn : exn -> message := "ltac2" "message_of_exn". (** Panics if there is more than one goal under focus. *) Ltac2 @ external concat : message -> message -> message := "ltac2" "message_concat". + +Module Format. + +(** Only for internal use. *) + +Ltac2 @ external stop : unit -> ('a, 'b, 'c, 'a) format := "ltac2" "format_stop". + +Ltac2 @ external string : ('a, 'b, 'c, 'd) format -> + (string -> 'a, 'b, 'c, 'd) format := "ltac2" "format_string". + +Ltac2 @ external int : ('a, 'b, 'c, 'd) format -> + (int -> 'a, 'b, 'c, 'd) format := "ltac2" "format_int". + +Ltac2 @ external constr : ('a, 'b, 'c, 'd) format -> + (constr -> 'a, 'b, 'c, 'd) format := "ltac2" "format_constr". + +Ltac2 @ external ident : ('a, 'b, 'c, 'd) format -> + (ident -> 'a, 'b, 'c, 'd) format := "ltac2" "format_ident". + +Ltac2 @ external literal : string -> ('a, 'b, 'c, 'd) format -> + ('a, 'b, 'c, 'd) format := "ltac2" "format_literal". + +Ltac2 @ external alpha : ('a, 'b, 'c, 'd) format -> + (('b -> 'r -> 'c) -> 'r -> 'a, 'b, 'c, 'd) format := "ltac2" "format_alpha". + +Ltac2 @ external kfprintf : (message -> 'r) -> ('a, unit, message, 'r) format -> 'a := + "ltac2" "format_kfprintf". + +End Format. diff --git a/user-contrib/Ltac2/Printf.v b/user-contrib/Ltac2/Printf.v new file mode 100644 index 0000000000..e2470ed1c3 --- /dev/null +++ b/user-contrib/Ltac2/Printf.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Ltac2.Message. + +(** This file defines a printf notation for easiness of writing messages *) + +(** + + The built-in "format" notation scope can be used to create well-typed variadic + printing commands following a printf-like syntax. The "format" scope parses + quoted strings which contain either raw string data or printing + specifications. Raw strings will be output verbatim as if they were passed + to Ltac2.Message.of_string. + + Printing specifications are of the form + + << '%' type >> + + where the type value defines which kind of arguments will be accepted and + how they will be printed. They can take the following values. + + - << i >>: takes an argument of type int and behaves as Message.of_int + - << I >>: takes an argument of type ident and behaves as Message.of_ident + - << s >>: takes an argument of type string and behaves as Message.of_string + - << t >>: takes an argument of type constr and behaves as Message.of_constr + - << a >>: takes two arguments << f >> of type << (unit -> 'a -> message) >> + and << x >> of type << 'a >> and behaves as << f () x >> + - << % >>: outputs << % >> verbatim + + TODO: add printing modifiers. + +*) + +Ltac2 printf fmt := Format.kfprintf print fmt. +Ltac2 fprintf fmt := Format.kfprintf (fun x => x) fmt. + +(** The two following notations are made available when this module is imported. + + - printf will parse a format and generate a function taking the + corresponding arguments ant printing the resulting message as per + Message.print. In particular when fully applied it has type unit. + - fprintf behaves similarly but return the message as a value instead of + printing it. + +*) + +Ltac2 Notation "printf" fmt(format) := printf fmt. +Ltac2 Notation "fprintf" fmt(format) := fprintf fmt. diff --git a/user-contrib/Ltac2/dune b/user-contrib/Ltac2/dune index 90869a46a0..b90bae10a3 100644 --- a/user-contrib/Ltac2/dune +++ b/user-contrib/Ltac2/dune @@ -1,14 +1,14 @@ (coq.theory (name Ltac2) - (package coq) + (package coq-stdlib) (synopsis "Ltac2 tactic language") - (libraries coq.plugins.ltac2)) + (libraries coq-core.plugins.ltac2)) (library (name ltac2_plugin) - (public_name coq.plugins.ltac2) + (public_name coq-core.plugins.ltac2) (synopsis "Ltac2 plugin") (modules_without_implementation tac2expr tac2qexpr tac2types) - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_ltac2)) diff --git a/user-contrib/Ltac2/plugin_base.dune b/user-contrib/Ltac2/plugin_base.dune deleted file mode 100644 index 711e9b95d3..0000000000 --- a/user-contrib/Ltac2/plugin_base.dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name ltac2_plugin) - (public_name coq.plugins.ltac2) - (synopsis "Coq's Ltac2 plugin") - (modules_without_implementation tac2expr tac2qexpr tac2types) - (libraries coq.plugins.ltac)) diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 241ca7ad66..948a359124 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -44,6 +44,9 @@ let open_constr_no_classes_flags = module Value = Tac2ffi open Value +let val_format = Tac2print.val_format +let format = repr_ext val_format + let core_prefix path n = KerName.make path (Label.of_id (Id.of_string_soft n)) let std_core n = core_prefix Tac2env.std_prefix n @@ -250,6 +253,79 @@ let () = define2 "message_concat" pp pp begin fun m1 m2 -> return (Value.of_pp (Pp.app m1 m2)) end +let () = define0 "format_stop" begin + return (Value.of_ext val_format []) +end + +let () = define1 "format_string" format begin fun s -> + return (Value.of_ext val_format (Tac2print.FmtString :: s)) +end + +let () = define1 "format_int" format begin fun s -> + return (Value.of_ext val_format (Tac2print.FmtInt :: s)) +end + +let () = define1 "format_constr" format begin fun s -> + return (Value.of_ext val_format (Tac2print.FmtConstr :: s)) +end + +let () = define1 "format_ident" format begin fun s -> + return (Value.of_ext val_format (Tac2print.FmtIdent :: s)) +end + +let () = define2 "format_literal" string format begin fun lit s -> + return (Value.of_ext val_format (Tac2print.FmtLiteral (Bytes.to_string lit) :: s)) +end + +let () = define1 "format_alpha" format begin fun s -> + return (Value.of_ext val_format (Tac2print.FmtAlpha :: s)) +end + +let () = define2 "format_kfprintf" closure format begin fun k fmt -> + let open Tac2print in + let fold accu = function + | FmtLiteral _ -> accu + | FmtString | FmtInt | FmtConstr | FmtIdent -> 1 + accu + | FmtAlpha -> 2 + accu + in + let pop1 l = match l with [] -> assert false | x :: l -> (x, l) in + let pop2 l = match l with [] | [_] -> assert false | x :: y :: l -> (x, y, l) in + let arity = List.fold_left fold 0 fmt in + let rec eval accu args fmt = match fmt with + | [] -> apply k [of_pp accu] + | tag :: fmt -> + match tag with + | FmtLiteral s -> + eval (Pp.app accu (Pp.str s)) args fmt + | FmtString -> + let (s, args) = pop1 args in + let pp = Pp.str (Bytes.to_string (to_string s)) in + eval (Pp.app accu pp) args fmt + | FmtInt -> + let (i, args) = pop1 args in + let pp = Pp.int (to_int i) in + eval (Pp.app accu pp) args fmt + | FmtConstr -> + let (c, args) = pop1 args in + let c = to_constr c in + pf_apply begin fun env sigma -> + let pp = Printer.pr_econstr_env env sigma c in + eval (Pp.app accu pp) args fmt + end + | FmtIdent -> + let (i, args) = pop1 args in + let pp = Id.print (to_ident i) in + eval (Pp.app accu pp) args fmt + | FmtAlpha -> + let (f, x, args) = pop2 args in + Tac2ffi.apply (to_closure f) [of_unit (); x] >>= fun pp -> + eval (Pp.app accu (to_pp pp)) args fmt + in + let eval v = eval (Pp.mt ()) v fmt in + if Int.equal arity 0 then eval [] + else return (Tac2ffi.of_closure (Tac2ffi.abstract arity eval)) +end + (** Array *) let () = define0 "array_empty" begin @@ -1629,6 +1705,7 @@ let () = add_expr_scope "pose" q_pose Tac2quote.of_pose let () = add_expr_scope "assert" q_assert Tac2quote.of_assertion let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching +let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml index a54eb45f61..7a53b577b6 100644 --- a/user-contrib/Ltac2/tac2print.ml +++ b/user-contrib/Ltac2/tac2print.ml @@ -489,3 +489,51 @@ let () = | _ -> assert false in register_val_printer kn { val_printer } + +(** {5 Ltac2 primitive} *) + +type format = +| FmtString +| FmtInt +| FmtConstr +| FmtIdent +| FmtLiteral of string +| FmtAlpha + +let val_format = Tac2dyn.Val.create "format" + +exception InvalidFormat + +let parse_format (s : string) : format list = + let len = String.length s in + let buf = Buffer.create len in + let rec parse i accu = + if len <= i then accu + else match s.[i] with + | '%' -> parse_argument (i + 1) accu + | _ -> + let i' = parse_literal i in + if Int.equal i i' then parse i' accu + else + let lit = Buffer.contents buf in + let () = Buffer.clear buf in + parse i' (FmtLiteral lit :: accu) + and parse_literal i = + if len <= i then i + else match s.[i] with + | '%' -> i + | c -> + let () = Buffer.add_char buf c in + parse_literal (i + 1) + and parse_argument i accu = + if len <= i then raise InvalidFormat + else match s.[i] with + | '%' -> parse (i + 1) (FmtLiteral "%" :: accu) + | 's' -> parse (i + 1) (FmtString :: accu) + | 'i' -> parse (i + 1) (FmtInt :: accu) + | 'I' -> parse (i + 1) (FmtIdent :: accu) + | 't' -> parse (i + 1) (FmtConstr :: accu) + | 'a' -> parse (i + 1) (FmtAlpha :: accu) + | _ -> raise InvalidFormat + in + parse 0 [] diff --git a/user-contrib/Ltac2/tac2print.mli b/user-contrib/Ltac2/tac2print.mli index df5b03f82a..6bb4884666 100644 --- a/user-contrib/Ltac2/tac2print.mli +++ b/user-contrib/Ltac2/tac2print.mli @@ -46,3 +46,19 @@ val pr_valexpr : Environ.env -> Evd.evar_map -> valexpr -> 'a glb_typexpr -> Pp. val int_name : unit -> (int -> string) (** Create a function that give names to integers. The names are generated on the fly, in the order they are encountered. *) + +(** {5 Ltac2 primitives}*) + +type format = +| FmtString +| FmtInt +| FmtConstr +| FmtIdent +| FmtLiteral of string +| FmtAlpha + +val val_format : format list Tac2dyn.Val.tag + +exception InvalidFormat + +val parse_format : string -> format list diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index 90f8008dc2..d1a72fcfd1 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -35,6 +35,7 @@ let prefix_gen n = let control_prefix = prefix_gen "Control" let pattern_prefix = prefix_gen "Pattern" let array_prefix = prefix_gen "Array" +let format_prefix = MPdot (prefix_gen "Message", Label.make "Format") let kername prefix n = KerName.make prefix (Label.of_id (Id.of_string_soft n)) let std_core n = kername Tac2env.std_prefix n @@ -75,6 +76,9 @@ let of_tuple ?loc el = match el with let len = List.length el in CAst.make ?loc @@ CTacApp (CAst.make ?loc @@ CTacCst (AbsKn (Tuple len)), el) +let of_string {loc;v=n} = + CAst.make ?loc @@ CTacAtm (AtmStr n) + let of_int {loc;v=n} = CAst.make ?loc @@ CTacAtm (AtmInt n) @@ -489,3 +493,27 @@ let of_assertion {loc;v=ast} = match ast with let id = of_anti of_ident id in let c = of_constr c in std_constructor ?loc "AssertValue" [id; c] + +let of_format accu = function +| Tac2print.FmtString -> + CAst.make @@ CTacApp (global_ref (kername format_prefix "string"), [accu]) +| Tac2print.FmtInt -> + CAst.make @@ CTacApp (global_ref (kername format_prefix "int"), [accu]) +| Tac2print.FmtConstr -> + CAst.make @@ CTacApp (global_ref (kername format_prefix "constr"), [accu]) +| Tac2print.FmtIdent -> + CAst.make @@ CTacApp (global_ref (kername format_prefix "ident"), [accu]) +| Tac2print.FmtLiteral lit -> + let s = of_string (CAst.make lit) in + CAst.make @@ CTacApp (global_ref (kername format_prefix "literal"), [s; accu]) +| Tac2print.FmtAlpha -> + CAst.make @@ CTacApp (global_ref (kername format_prefix "alpha"), [accu]) + +let of_format { v = fmt; loc } = + let fmt = + try Tac2print.parse_format fmt + with Tac2print.InvalidFormat -> + CErrors.user_err ?loc (str "Invalid format") + in + let stop = CAst.make @@ CTacApp (global_ref (kername format_prefix "stop"), [of_tuple []]) in + List.fold_left of_format stop fmt diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli index f9c41b57dc..fcd1339cd7 100644 --- a/user-contrib/Ltac2/tac2quote.mli +++ b/user-contrib/Ltac2/tac2quote.mli @@ -85,6 +85,8 @@ val of_constr_matching : constr_matching -> raw_tacexpr val of_goal_matching : goal_matching -> raw_tacexpr +val of_format : lstring -> raw_tacexpr + (** {5 Generic arguments} *) val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag diff --git a/vernac/dune b/vernac/dune index ba361b1377..7319b1353c 100644 --- a/vernac/dune +++ b/vernac/dune @@ -1,7 +1,7 @@ (library (name vernac) (synopsis "Coq's Vernacular Language") - (public_name coq.vernac) + (public_name coq-core.vernac) (wrapped false) (libraries tactics parsing)) |