diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-common.sh | 28 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 4 | ||||
| -rwxr-xr-x | dev/ci/gitlab.bat | 15 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08552-gares-elpi-11.sh | 5 | ||||
| -rw-r--r-- | dev/doc/changes.md | 9 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 24 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 2 |
9 files changed, 61 insertions, 30 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 7af648f0a6..4acc0e86cf 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,6 +8,7 @@ export NJOBS if [ -n "${GITLAB_CI}" ]; then + # Gitlab build, Coq installed into `_install_ci` export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" @@ -15,18 +16,29 @@ then then export CI_PULL_REQUEST="${CI_BRANCH#pr-}" fi +elif [ -n "${TRAVIS}" ]; +then + # Travis build, `-local` passed to `configure` + export OCAMLPATH="$PWD:$OCAMLPATH" + export COQBIN="$PWD/bin" + export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" + export CI_BRANCH="$TRAVIS_BRANCH" +elif [ -d "$PWD/_build/install/default/" ]; +then + # Dune build + export OCAMLPATH="$PWD/_build/install/default/lib/" + export COQBIN="$PWD/_build/install/default/bin" + export COQLIB="$PWD/_build/install/default/lib/coq" + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH else - if [ -n "${TRAVIS}" ]; - then - export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" - export CI_BRANCH="$TRAVIS_BRANCH" - else # assume local - CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" - export CI_BRANCH - fi + # We assume we are in `-profile devel` build, thus `-local` is set export OCAMLPATH="$PWD:$OCAMLPATH" export COQBIN="$PWD/bin" + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH fi + export PATH="$COQBIN:$PATH" # Coq's tools need an ending slash :S, we should fix them. diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index b04161918e..8d0f69626e 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-23-V01" +# CACHEKEY: "bionic_coq-V2018-09-24-V01" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -38,7 +38,7 @@ ENV COMPILER="4.02.3" # `num` does not have a version number as the right version to install varies # with the compiler version. ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \ - CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8" + CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV CAMLP5_VER="6.14" \ diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 31bd65af08..a848c49d75 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -8,23 +8,24 @@ TIME /T REM List currently used cygwin and target folders for debugging / maintenance purposes ECHO "Currently used cygwin folders" -DIR C:\cygwin* +DIR C:\ci\cygwin* ECHO "Currently used target folders" -DIR C:\coq* +DIR C:\ci\coq* +ECHO "Root folders" +DIR C:\ if %ARCH% == 32 ( SET ARCHLONG=i686 - SET CYGROOT=C:\cygwin SET SETUP=setup-x86.exe ) if %ARCH% == 64 ( SET ARCHLONG=x86_64 - SET CYGROOT=C:\cygwin64 SET SETUP=setup-x86_64.exe ) -SET DESTCOQ=C:\coq%ARCH%_inst +SET CYGROOT=C:\ci\cygwin%ARCH% +SET DESTCOQ=C:\ci\coq%ARCH% CALL :MakeUniqueFolder %CYGROOT% CYGROOT CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ @@ -93,9 +94,9 @@ GOTO :EOF :CleanupFolders ECHO "Cleaning %CYGROOT%" - DEL /S /F /Q "%CYGROOT%" > NUL + RMDIR /S /Q "%CYGROOT%" ECHO "Cleaning %DESTCOQ%" - DEL /S /F /Q "%DESTCOQ%" > NUL + RMDIR /S /Q "%DESTCOQ%" GOTO :EOF :MakeUniqueFolder diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh new file mode 100644 index 0000000000..c08f44fc50 --- /dev/null +++ b/dev/ci/user-overlays/08552-gares-elpi-11.sh @@ -0,0 +1,5 @@ +#!/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/doc/changes.md b/dev/doc/changes.md index 4f3d793ed4..fdeb0abed4 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,12 @@ +## Changes between Coq 8.9 and Coq 8.10 + +### ML API + +Termops: + +- Internal printing functions have been placed under the + `Termops.Internal` namespace. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index bccd3fefb4..85bb04efe0 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -37,7 +37,7 @@ if [ -z "$GUESS_CHECKER" ]; then -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/romega \ + -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 \ diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ab679a71ce..e15fd776b2 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -64,8 +64,14 @@ let ppwf_paths x = pp (Rtree.pp_tree prrecarg x) let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma let rawdebug = ref false let ppevar evk = pp (Evar.print evk) -let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) -let ppeconstr x = pp (Termops.print_constr x) +let pr_constr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_env env sigma t +let pr_econstr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_econstr_env env sigma t +let ppconstr x = pp (pr_constr x) +let ppeconstr x = pp (pr_econstr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x @@ -95,9 +101,9 @@ let ppidmapgen l = pp (pridmapgen l) let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 - (Termops.print_constr (EConstr.of_constr c) ++ + (pr_constr c ++ (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ - Termops.print_constr (EConstr.of_constr c) ++ str">") ++ + pr_constr c ++ str">") ++ (if id = id0 then mt () else spc () ++ str "<canonical: " ++ Id.print id ++ str ">")))) @@ -106,7 +112,7 @@ let ppididmap = ppidmap (fun _ -> Id.print) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") - ++ str "," ++ spc () ++ Termops.print_constr c) + ++ str "," ++ spc () ++ pr_econstr c) let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) @@ -133,7 +139,7 @@ let safe_pr_global = function | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str ")") - | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ + | ConstructRef ((kn,i),j) -> pp (str "CONSTRUCTREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")") @@ -155,9 +161,9 @@ let ppdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) -let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n) -let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) -let pp_state_t n = pp (Reductionops.pr_state n) +let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n) +let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n) +let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 6b7960c92f..dd3908c25f 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -765,8 +765,6 @@ Conflicts exists between integers and constrs. %% plugins/ring \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}} \nlsep \TERM{ring}~\STAR{\tacconstr} -%% plugins/romega -\nlsep \TERM{romega} \SEPDEF \DEFNT{orient} \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$} diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 47cfeb98d7..ea126e2756 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -10,7 +10,7 @@ let ppripos (ri,pos) = | Reloc_annot a -> let sp,i = a.ci.ci_ind in print_string - ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") + ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> |