diff options
Diffstat (limited to 'dev')
48 files changed, 387 insertions, 310 deletions
diff --git a/dev/base_include b/dev/base_include index 67a7e87d78..0e12b57b36 100644 --- a/dev/base_include +++ b/dev/base_include @@ -176,7 +176,7 @@ open Mltop open Record open Coqloop open Vernacentries -open Vernacinterp +open Vernacextend open Vernac (* Various utilities *) diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index c3d895784e..71207bb040 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -434,7 +434,7 @@ function build_prep_overlay { # ------------------------------------------------------------------------------ function load_overlay_data { - if [ -n "${GITLAB_CI+}" ]; then + if [ -n "${GITLAB_CI-}" ]; then export CI_BRANCH="$CI_COMMIT_REF_NAME" if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then export CI_PULL_REQUEST="${CI_BRANCH#pr-}" diff --git a/dev/checker.dbg b/dev/checker.dbg deleted file mode 100644 index b5b7f0e6d3..0000000000 --- a/dev/checker.dbg +++ /dev/null @@ -1,7 +0,0 @@ -load_printer threads.cma -load_printer str.cma -load_printer clib.cma -load_printer dynlink.cma -load_printer config.cma -load_printer lib.cma -load_printer check.cma diff --git a/dev/checker_db b/dev/checker_db deleted file mode 100644 index fcb6f679ed..0000000000 --- a/dev/checker_db +++ /dev/null @@ -1,5 +0,0 @@ -source checker.dbg - -load_printer checker_printers.cmo - -source checker_printers.dbg diff --git a/dev/checker_dune_db b/dev/checker_dune_db deleted file mode 100644 index cdb6a4b809..0000000000 --- a/dev/checker_dune_db +++ /dev/null @@ -1,5 +0,0 @@ -source checker_dune.dbg - -load_printer checker_printers.cma - -source checker_printers.dbg diff --git a/dev/checker_printers.dbg b/dev/checker_printers.dbg deleted file mode 100644 index 9ebbd74834..0000000000 --- a/dev/checker_printers.dbg +++ /dev/null @@ -1,35 +0,0 @@ -install_printer Checker_printers.pP - -install_printer Checker_printers.ppfuture - -install_printer Checker_printers.ppid -install_printer Checker_printers.pplab -install_printer Checker_printers.ppmbid -install_printer Checker_printers.ppdir -install_printer Checker_printers.ppmp -install_printer Checker_printers.ppcon -install_printer Checker_printers.ppproj -install_printer Checker_printers.ppkn -install_printer Checker_printers.ppmind -install_printer Checker_printers.ppind - -install_printer Checker_printers.ppbigint - -install_printer Checker_printers.ppintset -install_printer Checker_printers.ppidset - -install_printer Checker_printers.ppidmapgen - -install_printer Checker_printers.ppididmap - -install_printer Checker_printers.ppuni -install_printer Checker_printers.ppuni_level -install_printer Checker_printers.ppuniverse_set -install_printer Checker_printers.ppuniverse_instance -install_printer Checker_printers.ppauniverse_context -install_printer Checker_printers.ppuniverse_context -install_printer Checker_printers.ppconstraints -install_printer Checker_printers.ppuniverse_context_future -install_printer Checker_printers.ppuniverses - -install_printer Checker_printers.pploc diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml deleted file mode 100644 index 40ae1a7b05..0000000000 --- a/dev/checker_printers.ml +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -open Pp -open Names -open Univ - -let pp x = Pp.pp_with Format.std_formatter x - -(** Future printer *) - -let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) - -(* name printers *) -let ppid id = pp (Id.print id) -let pplab l = pp (Label.print l) -let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) -let ppdir dir = pp (DirPath.print dir) -let ppmp mp = pp(str (ModPath.debug_to_string mp)) -let ppcon con = pp(Constant.debug_print con) -let ppproj con = pp(Constant.debug_print (Projection.constant con)) -let ppkn kn = pp(str (KerName.to_string kn)) -let ppmind kn = pp(MutInd.debug_print kn) -let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i) - -(* term printers *) -let ppbigint n = pp (str (Bigint.to_string n));; - -let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" -let ppintset l = pp (prset int (Int.Set.elements l)) -let ppidset l = pp (prset Id.print (Id.Set.elements l)) - -let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" - -let pridmap pr l = - let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in - prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) -let ppidmap pr l = pp (pridmap pr l) - -let pridmapgen l = - let dom = Id.Set.elements (Id.Map.domain l) in - if dom = [] then str "[]" else - str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]" -let ppidmapgen l = pp (pridmapgen l) - -let prididmap = pridmap (fun _ -> Id.print) -let ppididmap = ppidmap (fun _ -> Id.print) - -let pP s = pp (hov 0 s) - -(* proof printers *) -let ppuni u = pp(Universe.pr u) -let ppuni_level u = pp (Level.pr u) - -let ppuniverse_set l = pp (LSet.pr l) -let ppuniverse_instance l = pp (Instance.pr l) -let ppauniverse_context l = pp (AUContext.pr Level.pr l) -let ppuniverse_context l = pp (pr_universe_context Level.pr l) -let ppconstraints c = pp (pr_constraints Level.pr c) -let ppuniverse_context_future c = - let ctx = Future.force c in - ppuniverse_context ctx -let ppuniverses u = pp (Univ.pr_universes u) - -let pploc x = let (l,r) = Loc.unloc x in - print_string"(";print_int l;print_string",";print_int r;print_string")" diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli deleted file mode 100644 index 2f9500c5c3..0000000000 --- a/dev/checker_printers.mli +++ /dev/null @@ -1,54 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -(** Printers for the ocaml toplevel. *) - -val pp : Pp.t -> unit -val pP : Pp.t -> unit (* with surrounding box *) - -val ppfuture : 'a Future.computation -> unit - -val ppid : Names.Id.t -> unit -val pplab : Names.Label.t -> unit -val ppmbid : Names.MBId.t -> unit -val ppdir : Names.DirPath.t -> unit -val ppmp : Names.ModPath.t -> unit -val ppcon : Names.Constant.t -> unit -val ppproj : Names.Projection.t -> unit -val ppkn : Names.KerName.t -> unit -val ppmind : Names.MutInd.t -> unit -val ppind : Names.inductive -> unit - -val ppbigint : Bigint.bigint -> unit - -val ppintset : Int.Set.t -> unit -val ppidset : Names.Id.Set.t -> unit - -val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t -val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit - -val pridmapgen : 'a Names.Id.Map.t -> Pp.t -val ppidmapgen : 'a Names.Id.Map.t -> unit - -val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t -val ppididmap : Names.Id.t Names.Id.Map.t -> unit - -(* Universes *) -val ppuni : Univ.Universe.t -> unit -val ppuni_level : Univ.Level.t -> unit (* raw *) -val ppuniverse_set : Univ.LSet.t -> unit -val ppuniverse_instance : Univ.Instance.t -> unit -val ppauniverse_context : Univ.AUContext.t -> unit -val ppuniverse_context : Univ.UContext.t -> unit -val ppconstraints : Univ.Constraint.t -> unit -val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit -val ppuniverses : Univ.universes -> unit - -val pploc : Loc.t -> unit diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 50d4d21637..3137576207 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -70,6 +70,13 @@ : "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" ######################################################################## +# CoqHammer +######################################################################## +: "${coqhammer_CI_REF:=master}" +: "${coqhammer_CI_GITURL:=https://github.com/lukaszcz/coqhammer}" +: "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}" + +######################################################################## # Ltac2 ######################################################################## : "${ltac2_CI_REF:=master}" @@ -255,3 +262,10 @@ : "${aactactics_CI_REF:=master}" : "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" : "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}" + +######################################################################## +# paramcoq +######################################################################## +: "${paramcoq_CI_REF:=master}" +: "${paramcoq_CI_GITURL:=https://github.com/coq-community/paramcoq}" +: "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" diff --git a/dev/ci/ci-coqhammer.sh b/dev/ci/ci-coqhammer.sh new file mode 100755 index 0000000000..4384e6c828 --- /dev/null +++ b/dev/ci/ci-coqhammer.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coqhammer + +( cd "${CI_BUILD_DIR}/coqhammer" && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 7eeeb09372..c8e6fe690f 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download HoTT -( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate ) +( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh new file mode 100755 index 0000000000..c641af2abb --- /dev/null +++ b/dev/ci/ci-paramcoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download paramcoq + +( cd "${CI_BUILD_DIR}/paramcoq" && make && make install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 098c950b32..4ddb582414 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-23-V1" +# CACHEKEY: "bionic_coq-V2018-10-30-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -53,8 +53,8 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch -ENV COMPILER_EDGE="4.07.0" \ - CAMLP5_VER_EDGE="7.06" \ +ENV COMPILER_EDGE="4.07.1" \ + CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ BASE_OPAM_EDGE="dune-release.1.1.0" diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix new file mode 100644 index 0000000000..4c5cfd83da --- /dev/null +++ b/dev/ci/nix/CoLoR.nix @@ -0,0 +1,5 @@ +{ bignums }: + +{ + buildInputs = [ bignums ]; +} diff --git a/dev/ci/nix/CompCert.nix b/dev/ci/nix/CompCert.nix new file mode 100644 index 0000000000..db1721e5f5 --- /dev/null +++ b/dev/ci/nix/CompCert.nix @@ -0,0 +1,7 @@ +{ ocamlPackages }: + +{ + buildInputs = with ocamlPackages; [ ocaml findlib menhir ]; + configure = "./configure -ignore-coq-version x86_64-linux"; + make = "make all check-proof"; +} diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix new file mode 100644 index 0000000000..18c7750279 --- /dev/null +++ b/dev/ci/nix/Corn.nix @@ -0,0 +1,5 @@ +{ bignums, math-classes }: + +{ + buildInputs = [ bignums math-classes ]; +} diff --git a/dev/ci/nix/Elpi.nix b/dev/ci/nix/Elpi.nix new file mode 100644 index 0000000000..0a6ed20295 --- /dev/null +++ b/dev/ci/nix/Elpi.nix @@ -0,0 +1,4 @@ +{ ocamlPackages }: +{ + buildInputs = with ocamlPackages; [ ocaml findlib elpi ]; +} diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix new file mode 100644 index 0000000000..a86fb2c44a --- /dev/null +++ b/dev/ci/nix/GeoCoq.nix @@ -0,0 +1,5 @@ +{ mathcomp }: +{ + buildInputs = [ mathcomp ]; + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/HoTT.nix b/dev/ci/nix/HoTT.nix new file mode 100644 index 0000000000..dea0aeeb55 --- /dev/null +++ b/dev/ci/nix/HoTT.nix @@ -0,0 +1,6 @@ +{ autoconf, automake }: +{ + buildInputs = [ autoconf automake ]; + configure = "./autogen.sh && ./configure"; + make = "make all validate"; +} diff --git a/dev/ci/nix/VST.nix b/dev/ci/nix/VST.nix new file mode 100644 index 0000000000..3e2629a0b6 --- /dev/null +++ b/dev/ci/nix/VST.nix @@ -0,0 +1,6 @@ +{}: + +rec { + make = "make IGNORECOQVERSION=true"; + clean = "${make} clean"; +} diff --git a/dev/ci/nix/bedrock2.nix b/dev/ci/nix/bedrock2.nix new file mode 100644 index 0000000000..552d9297e2 --- /dev/null +++ b/dev/ci/nix/bedrock2.nix @@ -0,0 +1,5 @@ +{}: +{ + configure = "git submodule update --init --recursive"; + clean = "(cd deps/bbv && make clean); (cd deps/riscv-coq && make clean); (cd compiler && make clean); (cd bedrock2 && make clean)"; +} diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix new file mode 100644 index 0000000000..1d931c858e --- /dev/null +++ b/dev/ci/nix/bignums.nix @@ -0,0 +1,5 @@ +{ ocamlPackages }: + +{ + buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ]; +} diff --git a/dev/ci/nix/coq.nix b/dev/ci/nix/coq.nix new file mode 100644 index 0000000000..ecd280e58d --- /dev/null +++ b/dev/ci/nix/coq.nix @@ -0,0 +1,9 @@ +{ stdenv, callPackage, branch, wd }: + +let coq = callPackage wd { buildDoc = false; doInstallCheck = false; coq-version = "8.9"; }; in + +coq.overrideAttrs (o: { + name = "coq-local-${branch}"; + src = fetchGit "${wd}"; + enableParallelBuilding = true; +}) diff --git a/dev/ci/nix/coq_dpdgraph.nix b/dev/ci/nix/coq_dpdgraph.nix new file mode 100644 index 0000000000..611e2fcca5 --- /dev/null +++ b/dev/ci/nix/coq_dpdgraph.nix @@ -0,0 +1,7 @@ +{ autoconf, ocamlPackages }: + +{ + buildInputs = [ autoconf ] ++ (with ocamlPackages; [ ocaml findlib camlp5 ocamlgraph ]); + configure = "autoconf && ./configure"; + make = "make all test-suite"; +} diff --git a/dev/ci/nix/cross_crypto.nix b/dev/ci/nix/cross_crypto.nix new file mode 100644 index 0000000000..98f74f9474 --- /dev/null +++ b/dev/ci/nix/cross_crypto.nix @@ -0,0 +1,5 @@ +{}: +{ + configure = "git submodule update --init --recursive"; + clean = "make cleanall"; +} diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix new file mode 100644 index 0000000000..4acfae48e4 --- /dev/null +++ b/dev/ci/nix/default.nix @@ -0,0 +1,72 @@ +{ pkgs ? import <nixpkgs> {} +, branch +, wd +, project ? "xyz" +, bn ? "release" +}: + +with pkgs; + +# Coq from this directory +let coq = callPackage ./coq.nix { inherit branch wd; }; in + +# Third-party libraries, built with this Coq +let coqPackages = mkCoqPackages coq; in +let mathcomp = coqPackages.mathcomp.overrideAttrs (o: { + name = "coq-git-mathcomp-git"; + src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz; + }); in +let bignums = coqPackages.bignums.overrideAttrs (o: + if bn == "release" then {} else + if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else + { src = fetchTarball bn; } + ); in +let coqprime = coqPackages.coqprime.override { inherit coq bignums; }; in +let math-classes = + (coqPackages.math-classes.override { inherit coq bignums; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz"; + }); in + +let unicoq = callPackage ./unicoq.nix { inherit coq; }; in + +let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in + +# Environments for building CI libraries with this Coq +let projects = { + bedrock2 = callPackage ./bedrock2.nix {}; + bignums = callPackage ./bignums.nix {}; + CoLoR = callPackage ./CoLoR.nix {}; + CompCert = callPackage ./CompCert.nix {}; + coq_dpdgraph = callPackage ./coq_dpdgraph.nix {}; + Corn = callPackage ./Corn.nix {}; + cross_crypto = callPackage ./cross_crypto.nix {}; + Elpi = callPackage ./Elpi.nix {}; + fiat_crypto = callPackage ./fiat_crypto.nix {}; + fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; + flocq = callPackage ./flocq.nix {}; + GeoCoq = callPackage ./GeoCoq.nix {}; + HoTT = callPackage ./HoTT.nix {}; + math_classes = callPackage ./math_classes.nix {}; + mathcomp = {}; + mtac2 = callPackage ./mtac2.nix {}; + oddorder = callPackage ./oddorder.nix {}; + VST = callPackage ./VST.nix {}; +}; in + +if !builtins.hasAttr project projects +then throw "Unknown project “${project}”; choose from: ${pkgs.lib.concatStringsSep ", " (builtins.attrNames projects)}." +else + +let prj = projects."${project}"; in + +stdenv.mkDerivation { + name = "shell-for-${project}-in-${branch}"; + + buildInputs = [ coq ] ++ (prj.buildInputs or []); + + configure = prj.configure or "true"; + make = prj.make or "make"; + clean = prj.clean or "make clean"; + +} diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix new file mode 100644 index 0000000000..7b37e6e8e4 --- /dev/null +++ b/dev/ci/nix/fiat_crypto.nix @@ -0,0 +1,6 @@ +{ coqprime }: +{ + buildInputs = [ coqprime ]; + configure = "git submodule update --init --recursive && ulimit -s 32768"; + make = "make new-pipeline c-files"; +} diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix new file mode 100644 index 0000000000..3248665579 --- /dev/null +++ b/dev/ci/nix/fiat_crypto_legacy.nix @@ -0,0 +1,6 @@ +{}: + +{ + configure = "./etc/ci/remove_autogenerated.sh"; + make = "make print-old-pipeline-lite old-pipeline-lite lite-display"; +} diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix new file mode 100644 index 0000000000..e153043557 --- /dev/null +++ b/dev/ci/nix/flocq.nix @@ -0,0 +1,7 @@ +{ autoconf, automake }: + +{ + buildInputs = [ autoconf automake ]; + configure = "./autogen.sh && ./configure"; + make = "./remake"; +} diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix new file mode 100644 index 0000000000..b0fa2fe795 --- /dev/null +++ b/dev/ci/nix/math_classes.nix @@ -0,0 +1,6 @@ +{ bignums }: + +{ + buildInputs = [ bignums ]; + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix new file mode 100644 index 0000000000..9a2353c5cf --- /dev/null +++ b/dev/ci/nix/mtac2.nix @@ -0,0 +1,5 @@ +{ coq, unicoq }: +{ + buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix new file mode 100644 index 0000000000..3b8fdbab51 --- /dev/null +++ b/dev/ci/nix/oddorder.nix @@ -0,0 +1,4 @@ +{ mathcomp }: +{ + buildInputs = [ mathcomp ]; +} diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell new file mode 100755 index 0000000000..2e4462ed40 --- /dev/null +++ b/dev/ci/nix/shell @@ -0,0 +1,20 @@ +#!/usr/bin/env sh + +## This file should be run from the root of the Coq source tree + +BRANCH=$(git rev-parse --abbrev-ref HEAD) +echo "Branch: $BRANCH in $PWD" + +if [ "$#" -ne 1 ]; then + PROJECT="" +else + PROJECT="--argstr project $1" +fi + +if [ "$BN" ]; then + BN="--argstr bn ${BN}" +else + BN="" +fi + +nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq.nix new file mode 100644 index 0000000000..f10afd5680 --- /dev/null +++ b/dev/ci/nix/unicoq.nix @@ -0,0 +1,14 @@ +{ stdenv, fetchzip, coq }: + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-unicoq-0.0-git"; + src = fetchzip { + url = "https://github.com/vbgl/unicoq/archive/8b33e37700e92bfd404bf8bf9fe03f1be8928d97.tar.gz"; + sha256 = "0s4z0wjxlp56ccgzxgk04z7skw90rdnz39v730ffkgrjl38rr9il"; + }; + + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]); + + configurePhase = "coq_makefile -f Make -o Makefile"; + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; +} diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh new file mode 100755 index 0000000000..4605255d5e --- /dev/null +++ b/dev/ci/user-overlays/08515-command-atts.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then + ltac2_CI_REF=command-atts + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + Equations_CI_REF=command-atts + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + plugin_tutorial_CI_REF=command-atts + plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials +fi diff --git a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh new file mode 100644 index 0000000000..9d723dc7f2 --- /dev/null +++ b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh @@ -0,0 +1,11 @@ +_OVERLAY_BRANCH=name-abstract-univ-context + +if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + Elpi_CI_REF="$_OVERLAY_BRANCH" + Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + Equations_CI_REF="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh new file mode 100644 index 0000000000..8ad8cba243 --- /dev/null +++ b/dev/ci/user-overlays/08844-split-tactics.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then + Equations_CI_REF=split-tactics + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + ltac2_CI_REF=split-tactics + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + fiat_parsers_CI_REF=split-tactics + fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat +fi diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh new file mode 100644 index 0000000000..17eb5fffae --- /dev/null +++ b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then + + Equations_CI_REF=program-hook-obligation-subst + Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 000f21c254..318562338d 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -6,19 +6,21 @@ This document describes how patches, submitted as pull requests (PRs) on the ## Code owners -The [CODEOWNERS](../../.github/CODEOWNERS) file describes, for each part of the -system, two owners. One is the principal maintainer of the component, the other -is the secondary maintainer. +The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of +the code. Sometime there is one principal maintainer and one or several +secondary maintainer(s). Sometimes, it is a team of code owners and all of its +members act as principal maintainers for the component. When a PR is submitted, GitHub will automatically ask the principal -maintainer for a review. If the PR touches several parts, all the -corresponding principal maintainers will be asked for a review. +maintainer (or the code owner team) for a review. If the PR touches several +parts, all the corresponding owners will be asked for a review. Maintainers are never assigned as reviewer on their own PRs. -If a principal maintainer submits a PR that changes the component they own, they -must assign the secondary maintainer as reviewer. They should also do it if they -know they are not available to do the review. +If a principal maintainer submits a PR or is a co-author of a PR that is +submitted and this PR changes the component they own, they must request a +review from a secondary maintainer. They can also delegate the review if they +know they are not available to do it. ## Reviewing @@ -35,17 +37,29 @@ When maintainers receive a review request, they are expected to: REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. -In all cases, maintainers can delegate reviews to the other maintainer of the -same component, except if it would lead to a maintainer reviewing their own -patch. +When a PR received lots of comments or if the PR has not been opened for long +and the assignee thinks that some other developers might want to comment, +it is recommended that they announce their intention to merge and wait a full +working day (or more if deemed useful) before the actual merge, as a sort of +last call for comments. + +In all cases, maintainers can delegate reviews to the other maintainers, +except if it would lead to a maintainer reviewing their own patch. A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. +When none of the maintainers have commented nor self-assigned a PR in a delay +of five working days, any maintainer of another component who feels comfortable +reviewing the PR can assign it to themselves. To prevent misunderstandings, +maintainers should not hesitate to announce in advance when they shall be +unavailable for more than five working days. + (*) In case a component is touched in a trivial way (adding/removing one file in a `Makefile`, etc), or by applying a systematic refactoring process (global renaming for instance) that has been reviewed globally, the assignee can -say in a comment they think a review is not required and proceed with the merge. +say in a comment they think a review is not required from every code owner and +proceed with the merge. ### Breaking changes @@ -54,7 +68,8 @@ those external projects should have been prepared (cf. the relevant sub-section in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). -Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. +Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or +the [`dev/doc/changes.md`](changes.md) file. If overlays are missing, ask the author to prepare them and label the PR with the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. @@ -78,9 +93,9 @@ put the approriate label. Otherwise, they are expected to merge the PR using the When CI has a few failures which look spurious, restarting the corresponding jobs is a good way of ensuring this was indeed the case. -To restart a job on Travis, you should connect using your GitHub account; -being part of the Coq organization on GitHub should give you the permission -to do so. +To restart a job on Travis or on AppVeyor, you should connect using your GitHub +account; being part of the Coq organization on GitHub should give you the +permission to do so. To restart a job on GitLab CI, you should sign into GitLab (this can be done using a GitHub account); if you are part of the [Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry" @@ -93,9 +108,10 @@ When the PR has conflicts, the assignee can either: In both cases, CI should be run again. -In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix +In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR +is not a candidate for backporting), it is ok to fix the conflicts in the merge commit (following the same steps as below), and push -to `master` directly. Don't use the GitHub interface to fix these conflicts. +to `master` directly. DON'T USE the GitHub interface to fix these conflicts. To merge the PR proceed in the following way ``` diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0aeb30c4e8..c5ea88aaf6 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -81,7 +81,7 @@ or ``` dune exec dev/dune-dbg checker -(ocd) source checker_dune_db +(ocd) source dune_db ``` for the checker. Unfortunately, dependency handling here is not fully diff --git a/dev/doc/changes.md b/dev/doc/changes.md index eb5b9ee1d3..b1fdfafd3a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -32,6 +32,12 @@ Macros: - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are deprecated. Use TYPED AS instead. +- coqpp (.mlg) based VERNAC EXTEND accesses attributes through a `#[ x + = att ]` syntax, where `att : 'a Attributes.attribute` and `x` will + be bound with type `'a` in the expression, unlike the old system + where `atts : Vernacexpr.vernac_flags` was bound in the expression + and had to be manually parsed. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index 8f96ac223f..774552237a 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the `Refine.refine` primitive. ```ocaml -val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine typecheck t], [t] is a term with holes under some +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions @@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) ``` -In a first approximation, we can think of `'a Sigma.run` as -`evar_map -> 'a * evar_map`. What the function does is first evaluate the -`Constr.t Sigma.run` argument in the current proof state, and then use the -resulting term as a filler for the proof under focus. All evars that have been -created by the invocation of this thunk are then turned into new goals added in -the order of their creation. +What the function does is first evaluate the `t` argument in the +current proof state, and then use the resulting term as a filler for +the proof under focus. All evars that have been created by the +invocation of this thunk are then turned into new goals added in the +order of their creation. To see how we can use it, let us have a look at an idealized example, the `cut` tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` @@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order. ```ocaml let cut c = - let open Sigma in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (** In this block, we focus on one goal at a time indicated by gl *) let env = Proofview.Goal.env gl in (** Get the context of the goal, essentially [Γ] *) @@ -80,25 +78,22 @@ let cut c = let t = mkArrow c (Vars.lift 1 concl) in (** Build [X -> A]. Note the lifting of [A] due to being on the right hand side of the arrow. *) - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> (** All evars generated by this block will be added as goals *) - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + let sigma, f = Evarutil.new_evar env sigma t in (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity substitution for [Γ] is extracted from the [env] argument, so that one must be careful to pass the correct context here in order for the resulting term to be well-typed. The [p] return value is a proof term used to enforce sigma monotonicity. *) - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + let sigma, x = Evarutil.new_evar env sigma c in (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return [x := Γ ⊢ ?e2{Γ} : X]. *) let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) - Sigma (r, sigma, p +> q) - (** Fills the current hole with [r]. The [p +> q] thingy ensures - monotonicity of sigma. *) - end } - end } + end + end ``` The `Evarutil.new_evar` function is the preferred way to generate evars in @@ -3,18 +3,9 @@ (public_name coq.top_printers) (synopsis "Coq's Debug Printers") (wrapped false) - (modules :standard \ checker_printers) + (modules :standard) (libraries coq.toplevel coq.plugins.ltac)) -(library - (name checker_printers) - (public_name coq.checker_printers) - (synopsis "Coq's Debug Printers [for the Checker]") - (wrapped false) - (flags :standard -open Checklib) - (modules checker_printers) - (libraries coq.checklib)) - (rule (targets dune-dbg) (deps dune-dbg.in diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 464e026400..3f3df23fe1 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -2,10 +2,12 @@ # Run in a proper install dune env. case $1 in -checker) - ocamldebug `ocamlfind query -recursive -i-format coq.checker_printers` -I +threads -I dev _build/default/checker/main.bc - ;; -*) - ocamldebug `ocamlfind query -recursive -i-format coq.top_printers` -I +threads -I dev _build/default/topbin/coqtop_byte_bin.bc - ;; + checker) + exe=_build/default/checker/main.bc + ;; + *) + exe=_build/default/topbin/coqtop_byte_bin.bc + ;; esac + +ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index f45f6de529..cf95941de5 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -3,5 +3,5 @@ ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.07.0))) -(context (opam (switch 4.07.0+flambda))) +(context (opam (switch 4.07.1))) +(context (opam (switch 4.07.1+flambda))) diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 85bb04efe0..d330f517be 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -14,40 +14,24 @@ export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH -GUESS_CHECKER= -for arg in "$@"; do - if [ "${arg##*/}" = coqchk.byte ]; then - GUESS_CHECKER=1 - fi -done - -if [ -z "$GUESS_CHECKER" ]; then - exec $OCAMLDEBUG \ - -I $CAMLP5LIB -I +threads \ - -I $COQTOP \ - -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ - -I $COQTOP/library -I $COQTOP/engine \ - -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ - -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ - -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ - -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ - -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ - -I $COQTOP/plugins/firstorder \ - -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ - -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ - -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ - -I $COQTOP/plugins/ring \ - -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ - -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ - -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ - -I $COQTOP/ide \ - "$@" -else - exec $OCAMLDEBUG \ - -I $CAMLP5LIB -I +threads \ - -I $COQTOP \ - -I $COQTOP/config -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/checker \ - "$@" -fi +exec $OCAMLDEBUG \ + -I $CAMLP5LIB -I +threads \ + -I $COQTOP \ + -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ + -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ + -I $COQTOP/library -I $COQTOP/engine \ + -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ + -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ + -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ + -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ + -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ + -I $COQTOP/plugins/firstorder \ + -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ + -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ + -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ + -I $COQTOP/plugins/ring \ + -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ + -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ + -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ + -I $COQTOP/ide \ + "$@" diff --git a/dev/tools/change-header b/dev/tools/change-header index 61cc866602..687c02f4f1 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' modified=0 kept=0 -for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do +for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do headline=`head -n 1 $i` if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then # Has emacs header diff --git a/dev/top_printers.ml b/dev/top_printers.ml index fd08f9ffe8..f94e9acb72 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -509,41 +509,23 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Genarg -open Stdarg -open Egramml - let _ = - try - Vernacinterp.vinterp_add false ("PrintConstr", 0) - (function - [c] when genarg_tag c = unquote (topwit wit_constr) && true -> - let c = out_gen (rawwit wit_constr) c in - (fun ~atts ~st -> in_current_context econstr_display c; st) - | _ -> failwith "Vernac extension: cannot occur") - with - e -> pp (CErrors.print e) -let _ = - extend_vernac_command_grammar ("PrintConstr", 0) None - [GramTerminal "PrintConstr"; - GramNonTerminal - (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] + let open Vernacextend in + let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in + let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in + let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in + let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in + Vernacextend.vernac_extend ~command:"PrintConstr" [cmd] let _ = - try - Vernacinterp.vinterp_add false ("PrintPureConstr", 0) - (function - [c] when genarg_tag c = unquote (topwit wit_constr) && true -> - let c = out_gen (rawwit wit_constr) c in - (fun ~atts ~st -> in_current_context print_pure_econstr c; st) - | _ -> failwith "Vernac extension: cannot occur") - with - e -> pp (CErrors.print e) -let _ = - extend_vernac_command_grammar ("PrintPureConstr", 0) None - [GramTerminal "PrintPureConstr"; - GramNonTerminal - (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] + let open Vernacextend in + let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in + let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in + let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in + let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in + Vernacextend.vernac_extend ~command:"PrintPureConstr" [cmd] (* Setting printer of unbound global reference *) open Names |