diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/ci/README.md | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh | 14 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh | 6 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 21 | ||||
| -rw-r--r-- | dev/doc/changes.md | 4 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 2 | ||||
| -rw-r--r-- | dev/dune | 3 | ||||
| -rwxr-xr-x | dev/dune-dbg.in | 2 | ||||
| -rw-r--r-- | dev/top_printers.mli | 6 |
10 files changed, 46 insertions, 15 deletions
diff --git a/dev/base_include b/dev/base_include index 0e12b57b36..d2e8f6d092 100644 --- a/dev/base_include +++ b/dev/base_include @@ -135,7 +135,6 @@ open Pfedit open Proof open Proof_using open Proof_global -open Proof_type open Redexpr open Refiner open Tacmach diff --git a/dev/ci/README.md b/dev/ci/README.md index 4709247549..7ed90f524c 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -179,7 +179,7 @@ Currently available artifacts are: + Coq's Reference Manual [master branch] https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + Coq's Standard Library Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base + Coq's ML API Documentation [master branch] https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh new file mode 100644 index 0000000000..b05d02c5be --- /dev/null +++ b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh @@ -0,0 +1,14 @@ +_OVERLAY_BRANCH=clean-transp-state + +if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + unicoq_CI_REF="$_OVERLAY_BRANCH" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + + equations_CI_REF="$_OVERLAY_BRANCH" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + mtac2_CI_REF="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh new file mode 100644 index 0000000000..c8bea0c868 --- /dev/null +++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then + + equations_CI_REF=legacy_proof_eng_clean + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index c5ea88aaf6..3609171b82 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,7 +10,8 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq +Dune >= 1.5.0 is recommended, see `dune-project` for the minimum +required version; type `dune build` to build the base Coq libraries. No call to `./configure` is needed. Dune will get confused if it finds leftovers of in-tree compilation, @@ -49,14 +50,25 @@ The default dune target is `dune build` (or `dune build @install`), which will scan all sources in the Coq tree and then build the whole project, creating an "install" overlay in `_build/install/default`. -You can build some other target by doing `dune build $TARGET`. +You can build some other target by doing `dune build $TARGET`, where +`$TARGET` can be a `.cmxa`, a binary, a file that Dune considers a +target, an alias, etc... In order to build a single package, you can do `dune build $PACKAGE.install`. +A very useful target is `dune build @check`, that will compile all the +ml files in quick mode. + Dune also provides targets for documentation, testing, and release builds, please see below. +## Documentation and test targets + +Coq's test-suite can be run with `dune runtest`. + +The documentation target is not implemented in Dune yet. + ## Developer shell You can create a developer shell with `dune utop $library`, where @@ -139,11 +151,6 @@ Note that due to https://github.com/ocaml/dune/issues/1401 , we must perform a full rebuild each time as otherwise Dune will remove the files. We hope to solve this in the future. -## Documentation and test targets - -The documentation and test suite targets for Coq are still not -implemented in Dune. - ## Planned and Advanced features Dune supports or will support extra functionality that may result very diff --git a/dev/doc/changes.md b/dev/doc/changes.md index b1fdfafd3a..30a2967259 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -19,6 +19,10 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 +- `Names.transparent_state` has been moved to its own module `TransparentState`. + This module gathers utility functions that used to be defined in several + places. + Coqlib: - Most functions from the `Coqlib` module have been deprecated in favor of diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 764d482957..e5e4f740bd 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -94,7 +94,7 @@ Tacexpr.glob_tactic_expr | | Tacinterp.eval_tactic (?) V -Proof_type.tactic +Proofview.V82.tac TODO: check with Hugo @@ -4,12 +4,13 @@ (synopsis "Coq's Debug Printers") (wrapped false) (modules :standard) + (optional) (libraries coq.toplevel coq.plugins.ltac)) (rule (targets dune-dbg) (deps dune-dbg.in - ../checker/main.bc + ../checker/coqchk.bc ../topbin/coqtop_byte_bin.bc ; This is not enough as the call to `ocamlfind` will fail :/ top_printers.cma) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 3f3df23fe1..80ad0500e0 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -3,7 +3,7 @@ # Run in a proper install dune env. case $1 in checker) - exe=_build/default/checker/main.bc + exe=_build/default/checker/coqchk.bc ;; *) exe=_build/default/topbin/coqtop_byte_bin.bc diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 63d7d58053..5eac3e2b9c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -101,7 +101,7 @@ val ppdelta : Mod_subst.delta_resolver -> unit val pp_idpred : Names.Id.Pred.t -> unit val pp_cpred : Names.Cpred.t -> unit -val pp_transparent_state : Names.transparent_state -> unit +val pp_transparent_state : TransparentState.t -> unit val pp_stack_t : Constr.t Reductionops.Stack.t -> unit val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit @@ -120,9 +120,9 @@ val ppclenv : Clenv.clausenv -> unit val ppgoalgoal : Goal.goal -> unit -val ppgoal : Proof_type.goal Evd.sigma -> unit +val ppgoal : Goal.goal Evd.sigma -> unit (* also print evar map *) -val ppgoalsigma : Proof_type.goal Evd.sigma -> unit +val ppgoalsigma : Goal.goal Evd.sigma -> unit val pphintdb : Hints.Hint_db.t -> unit val ppproofview : Proofview.proofview -> unit |