diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-math-classes.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 15 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06859-ejgallego-stm+top.sh | 6 | ||||
| -rw-r--r-- | dev/doc/changes.md | 6 |
6 files changed, 29 insertions, 6 deletions
diff --git a/dev/base_include b/dev/base_include index 2f7183dd63..2f5d8aa843 100644 --- a/dev/base_include +++ b/dev/base_include @@ -231,7 +231,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; -let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc) +let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc)) let _ = print_string diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 3608f7305d..ecc45735f1 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -847,7 +847,7 @@ function make_ocaml { function make_ocaml_tools { make_findlib - make_menhir + # make_menhir make_camlp5 } @@ -856,7 +856,7 @@ function make_ocaml_tools { function make_ocaml_libs { make_findlib make_lablgtk - make_stdint + # make_stdint } ##### FINDLIB Ocaml library manager ##### diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 4fc06e8956..6a064b2971 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -7,4 +7,4 @@ math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes" git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}" -( cd "${math_classes_CI_DIR}" && make && make install ) +( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index d04b9637c0..2ac4d21671 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -8,6 +8,17 @@ pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" -( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top ) +# Travis / Gitlab have different filesystem layout due to use of +# `-local`. We need to improve this divergence but if we use Dune this +# "local" oddity goes away automatically so not bothering... +if [ -d "$COQBIN/../lib/coq" ]; then + COQOCAMLLIB="$COQBIN/../lib/" + COQLIB="$COQBIN/../lib/coq/" +else + COQOCAMLLIB="$COQBIN/../" + COQLIB="$COQBIN/../" +fi -echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop +( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install ) + +echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh new file mode 100644 index 0000000000..ca0076b468 --- /dev/null +++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then + pidetop_CI_BRANCH=stm+top + pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index fb3f751db3..ff448abe81 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,12 @@ ### ML API +Misctypes + + Syntax for universe sorts and kinds has been moved from `Misctypes` + to `Glob_term`, as these are turned into kernel terms by + `Pretyping`. + Proof engine - More functions have been changed to use `EConstr`, notably the |