diff options
99 files changed, 646 insertions, 417 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/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/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). @@ -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 ea099eb52e..8fa1b97851 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/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. @@ -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/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/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/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/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/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/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)) |