diff options
Diffstat (limited to 'dev')
71 files changed, 432 insertions, 394 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 71207bb040..0dcabc0b97 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1645,7 +1645,7 @@ function make_addon_bignums { function make_addon_equations { installer_addon_dependency equations - if build_prep_overlay Equations; then + if build_prep_overlay equations; then installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" "" # Note: PATH is automatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH 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 4f89bbd34e..0000000000 --- a/dev/checker_printers.ml +++ /dev/null @@ -1,69 +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_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 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 8be9b87257..0000000000 --- a/dev/checker_printers.mli +++ /dev/null @@ -1,50 +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_context : Univ.UContext.t -> unit -val ppconstraints : Univ.Constraint.t -> unit -val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit - -val pploc : Loc.t -> unit 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/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh deleted file mode 100755 index 896a0ddf66..0000000000 --- a/dev/ci/ci-aac-tactics.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download aactactics - -( cd "${CI_BUILD_DIR}/aactactics" && make && make install ) diff --git a/dev/ci/ci-aac_tactics.sh b/dev/ci/ci-aac_tactics.sh new file mode 100755 index 0000000000..19f1f43746 --- /dev/null +++ b/dev/ci/ci-aac_tactics.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download aac_tactics + +( cd "${CI_BUILD_DIR}/aac_tactics" && make && make install ) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 50d4d21637..4d5834eeb6 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}" @@ -106,16 +113,16 @@ ######################################################################## # CompCert ######################################################################## -: "${CompCert_CI_REF:=master}" -: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" -: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}" +: "${compcert_CI_REF:=master}" +: "${compcert_CI_GITURL:=https://github.com/AbsInt/CompCert}" +: "${compcert_CI_ARCHIVEURL:=${compcert_CI_GITURL}/archive}" ######################################################################## # VST ######################################################################## -: "${VST_CI_REF:=master}" -: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" -: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" +: "${vst_CI_REF:=master}" +: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}" ######################################################################## # cross-crypto @@ -146,7 +153,7 @@ : "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" ######################################################################## -# coq-dpdgraph +# coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" @@ -155,9 +162,9 @@ ######################################################################## # CoLoR ######################################################################## -: "${CoLoR_CI_REF:=master}" -: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" -: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" +: "${color_CI_REF:=master}" +: "${color_CI_GITURL:=https://github.com/fblanqui/color}" +: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}" ######################################################################## # SF @@ -189,16 +196,16 @@ ######################################################################## # Equations ######################################################################## -: "${Equations_CI_REF:=master}" -: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" -: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}" +: "${equations_CI_REF:=master}" +: "${equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" +: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}" ######################################################################## # Elpi ######################################################################## -: "${Elpi_CI_REF:=coq-master}" -: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" -: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" +: "${elpi_CI_REF:=coq-master}" +: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" +: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}" ######################################################################## # fcsl-pcm @@ -250,8 +257,15 @@ : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" ######################################################################## -# aac-tactics +# aac_tactics +######################################################################## +: "${aac_tactics_CI_REF:=master}" +: "${aac_tactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" +: "${aac_tactics_CI_ARCHIVEURL:=${aac_tactics_CI_GITURL}/archive}" + +######################################################################## +# paramcoq ######################################################################## -: "${aactactics_CI_REF:=master}" -: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" -: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}" +: "${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-color.sh b/dev/ci/ci-color.sh index dc696f69d9..a0094b1006 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download CoLoR +git_download color -( cd "${CI_BUILD_DIR}/CoLoR" && make ) +( cd "${CI_BUILD_DIR}/color" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 7a450d0d48..a5aa54144c 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -46,8 +46,11 @@ for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null . "${overlay}" done + +set +x # shellcheck source=ci-basic-overlay.sh . "${ci_dir}/ci-basic-overlay.sh" +set -x # [git_download project] will download [project] and unpack it # in [$CI_BUILD_DIR/project] if the folder does not exist already; diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 01c35ceb4a..59a85e4726 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download CompCert +git_download compcert -( cd "${CI_BUILD_DIR}/CompCert" && \ +( cd "${CI_BUILD_DIR}/compcert" && \ ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq_dpdgraph.sh index 2373ea6c62..2373ea6c62 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq_dpdgraph.sh 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-elpi.sh b/dev/ci/ci-elpi.sh index 9b4a06fd5b..d60bf34ba2 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Elpi +git_download elpi -( cd "${CI_BUILD_DIR}/Elpi" && make && make install ) +( cd "${CI_BUILD_DIR}/elpi" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 998d50faa7..b58a794da2 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Equations +git_download equations -( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \ +( cd "${CI_BUILD_DIR}/equations" && coq_makefile -f _CoqProject -o Makefile && \ make && make test-suite && make examples && make install) 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/ci-plugin-tutorial.sh b/dev/ci/ci-plugin_tutorial.sh index 6c26a71a21..6c26a71a21 100755 --- a/dev/ci/ci-plugin-tutorial.sh +++ b/dev/ci/ci-plugin_tutorial.sh diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 0fec19205a..169d1a41db 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download VST +git_download vst -( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true ) +( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true ) 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/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh deleted file mode 100644 index d812df3ec0..0000000000 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_REF=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp -fi diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh deleted file mode 100644 index 575df07425..0000000000 --- a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh +++ /dev/null @@ -1,8 +0,0 @@ -_OVERLAY_BRANCH=pure-sharing-flag - -if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - mtac2_CI_BRANCH="$_OVERLAY_BRANCH" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - -fi diff --git a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh deleted file mode 100644 index 019cb8054d..0000000000 --- a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then - cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification - cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto -fi diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh deleted file mode 100644 index 3a6480a5a1..0000000000 --- a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then - - ltac2_CI_BRANCH=master+globenv-coq-pr7288 - ltac2_CI_GITURL=https://github.com/herbelin/ltac2 - -fi 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/08456-fix-6764.sh b/dev/ci/user-overlays/08456-fix-6764.sh deleted file mode 100644 index 3b951d9c07..0000000000 --- a/dev/ci/user-overlays/08456-fix-6764.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8456" ] || [ "$CI_BRANCH" = "fix-6764" ]; then - Elpi_CI_REF=overlay/8456 -fi diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh deleted file mode 100755 index 4605255d5e..0000000000 --- a/dev/ci/user-overlays/08515-command-atts.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/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/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh deleted file mode 100644 index c08f44fc50..0000000000 --- a/dev/ci/user-overlays/08552-gares-elpi-11.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then - Elpi_CI_REF=coq-master-elpi-1.1 -fi diff --git a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh deleted file mode 100644 index 484ad8f9e6..0000000000 --- a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh +++ /dev/null @@ -1,11 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8554" ] || [ "$CI_BRANCH" = "master+fix8553-change-under-binders" ]; then - - ltac2_CI_BRANCH=master+fix-pr8554-change-takes-env - ltac2_CI_REF=master+fix-pr8554-change-takes-env - ltac2_CI_GITURL=https://github.com/herbelin/ltac2 - - Equations_CI_BRANCH=master+fix-pr8554-change-takes-env - Equations_CI_REF=master+fix-pr8554-change-takes-env - Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh deleted file mode 100644 index 41c2ad6fef..0000000000 --- a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then - - ltac2_CI_REF=rm-section-path - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - Equations_CI_REF=rm-section-path - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -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 deleted file mode 100644 index 9d723dc7f2..0000000000 --- a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh +++ /dev/null @@ -1,11 +0,0 @@ -_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/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh deleted file mode 100644 index bd3e1bf7ff..0000000000 --- a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then - plugin_tutorial_CI_REF=pr8671-fix - plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials - -fi diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh deleted file mode 100644 index 98530c825a..0000000000 --- a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then - - Elpi_CI_REF=kernel-entries-cleanup - Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - Equations_CI_REF=kernel-entries-cleanup - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh deleted file mode 100644 index 81ed91f52b..0000000000 --- a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then - - Elpi_CI_REF=master+generalized-evar-printers-pr8688 - Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh deleted file mode 100644 index b3a9f67e00..0000000000 --- a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then - - # ltac2_CI_REF=rm-section-path - # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - plugin_tutorial_CI_REF=vernac+monify_hook - plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials - - Elpi_CI_REF=vernac+monify_hook - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - Equations_CI_REF=vernac+monify_hook - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh deleted file mode 100644 index 8ad8cba243..0000000000 --- a/dev/ci/user-overlays/08844-split-tactics.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/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/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh new file mode 100644 index 0000000000..08112d3054 --- /dev/null +++ b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then + + aactactics_CI_REF=ltac+use_atts_in_ast + aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics + + coqhammer_CI_REF=ltac+use_atts_in_ast + coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer + + Equations_CI_REF=ltac+use_atts_in_ast + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=ltac+use_atts_in_ast + mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh new file mode 100644 index 0000000000..1c5157ba12 --- /dev/null +++ b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then + + quickchick_CI_REF=lib+better_boot_coqproject + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh new file mode 100644 index 0000000000..61ffa4a197 --- /dev/null +++ b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then + + ltac2_CI_REF=vernac+move_extend_ast + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + +fi diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh deleted file mode 100644 index 76aa37d380..0000000000 --- a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh +++ /dev/null @@ -1,5 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then - HoTT_CI_REF=fix-for-numeral-notations - HoTT_CI_GITURL=https://github.com/JasonGross/HoTT - HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive -fi 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 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 @@ -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/tools/create_overlays.sh b/dev/tools/create_overlays.sh new file mode 100755 index 0000000000..314ac07e68 --- /dev/null +++ b/dev/tools/create_overlays.sh @@ -0,0 +1,78 @@ +#!/usr/bin/env bash + +# TODO: +# +# - Check if the branch already exists in the remote => checkout +# - Better error handling +# - Just checkout, don't build +# - Rebase functionality +# + +set -x +set -e +set -o pipefail + +# setup_contrib_git("_build_ci/fiat", "https://github.com/ejgallego/fiat-core.git") +setup_contrib_git() { + + local _DIR=$1 + local _GITURL=$2 + + ( cd $_DIR + git checkout -b $OVERLAY_BRANCH || true # allow the branch to exist already + git remote add $DEVELOPER_NAME $_GITURL || true # allow the remote to exist already + ) + +} + +if [ $# -lt 3 ]; then + echo "usage: $0 github_username pr_number contrib1 ... contribN" + exit 1 +fi + +set +x +. dev/ci/ci-basic-overlay.sh +set -x + +DEVELOPER_NAME=$1 +shift +PR_NUMBER=$1 +shift +OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD) +OVERLAY_FILE=$(mktemp overlay-XXXX) + +# Create the overlay file +printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then \n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" + +# We first try to build the contribs +while test $# -gt 0 +do + _CONTRIB_NAME=$1 + _CONTRIB_GITURL=${_CONTRIB_NAME}_CI_GITURL + _CONTRIB_GITURL=${!_CONTRIB_GITURL} + echo "Processing Contrib $_CONTRIB_NAME" + + # check _CONTRIB_GIT exists and it is of the from github... + + _CONTRIB_DIR=_build_ci/$_CONTRIB_NAME + + # extract the relevant part of the repository + _CONTRIB_GITSUFFIX=${_CONTRIB_GITURL#https://github.com/*/} + _CONTRIB_GITURL="https://github.com/$DEVELOPER_NAME/$_CONTRIB_GITSUFFIX" + _CONTRIB_GITPUSHURL="git@github.com:$DEVELOPER_NAME/${_CONTRIB_GITSUFFIX}.git" + + # This should work better: for example we should be able not to + # build but just to checkout. + make ci-$_CONTRIB_NAME || true + setup_contrib_git $_CONTRIB_DIR $_CONTRIB_GITPUSHURL + + echo " ${_CONTRIB_NAME}_CI_REF=$OVERLAY_BRANCH" >> $OVERLAY_FILE + echo " ${_CONTRIB_NAME}_CI_GITURL=$_CONTRIB_GITURL" >> $OVERLAY_FILE + echo "" >> $OVERLAY_FILE + shift +done + +# End the file; copy to overlays folder. +echo "fi" >> $OVERLAY_FILE +PR_NUMBER=$(printf '%05d' "$PR_NUMBER") +mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-$OVERLAY_BRANCH.sh diff --git a/dev/top_printers.ml b/dev/top_printers.ml index fd08f9ffe8..4287702b3a 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 _ = VtQuery,VtNow in + let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in + 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 _ = VtQuery,VtNow in + let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in + vernac_extend ~command:"PrintPureConstr" [cmd] (* Setting printer of unbound global reference *) open Names diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 63d7d58053..eaa12ff702 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 |