aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh2
-rw-r--r--dev/checker_printers.ml4
-rw-r--r--dev/checker_printers.mli4
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile8
-rw-r--r--dev/ci/user-overlays/08889-mattam-program-obl-subst.sh6
-rw-r--r--dev/dune-workspace.all4
-rw-r--r--dev/ocamldebug-coq.run58
7 files changed, 34 insertions, 52 deletions
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_printers.ml b/dev/checker_printers.ml
index 40ae1a7b05..4f89bbd34e 100644
--- a/dev/checker_printers.ml
+++ b/dev/checker_printers.ml
@@ -59,15 +59,11 @@ let pP s = pp (hov 0 s)
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
index 2f9500c5c3..8be9b87257 100644
--- a/dev/checker_printers.mli
+++ b/dev/checker_printers.mli
@@ -43,12 +43,8 @@ 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/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 098c950b32..0439d566fd 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-11-07-V1"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \
CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
# BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV CAMLP5_VER="7.03" \
+ENV CAMLP5_VER="7.06" \
COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
# base switch
@@ -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/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/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 \
+ "$@"
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:42:27 +0000