aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include2
-rw-r--r--dev/build/windows/makecoq_mingw.sh71
-rw-r--r--dev/build/windows/patches_coq/lablgtk-2.18.6.patch101
-rw-r--r--dev/ci/appveyor.sh10
-rwxr-xr-xdev/ci/ci-basic-overlay.sh12
-rw-r--r--dev/ci/ci-common.sh2
-rwxr-xr-xdev/ci/ci-ext-lib.sh16
-rwxr-xr-xdev/ci/ci-pidetop.sh4
-rwxr-xr-xdev/ci/ci-quickchick.sh18
-rw-r--r--dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh14
-rw-r--r--dev/doc/changes.md21
-rw-r--r--dev/vm_printers.ml1
12 files changed, 237 insertions, 35 deletions
diff --git a/dev/base_include b/dev/base_include
index 8d81ca3e0..fc38305cc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -189,7 +189,7 @@ let qid = Libnames.qualid_of_string;;
(* parsing of terms *)
let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
+let parse_vernac = Pcoq.parse_string Pvernac.Vernac_.vernac_control;;
let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
(* build a term of type glob_constr without type-checking or resolution of
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index ecc45735f..508dcf5fb 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -480,19 +480,19 @@ function make_sed {
##### LIBPNG #####
function make_libpng {
- build_conf_make_inst http://prdownloads.sourceforge.net/libpng libpng-1.6.18 tar.gz true
+ build_conf_make_inst http://prdownloads.sourceforge.net/libpng libpng-1.6.34 tar.gz true
}
##### PIXMAN #####
function make_pixman {
- build_conf_make_inst http://cairographics.org/releases pixman-0.32.8 tar.gz true
+ build_conf_make_inst http://cairographics.org/releases pixman-0.34.0 tar.gz true
}
##### FREETYPE #####
function make_freetype {
- build_conf_make_inst http://sourceforge.net/projects/freetype/files/freetype2/2.6.1 freetype-2.6.1 tar.bz2 true
+ build_conf_make_inst http://sourceforge.net/projects/freetype/files/freetype2/2.9.1 freetype-2.9.1 tar.bz2 true
}
##### EXPAT #####
@@ -508,7 +508,7 @@ function make_fontconfig {
make_expat
# CONFIGURE PARAMETERS
# build/install fails without --disable-docs
- build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.11.94 tar.gz true --disable-docs
+ build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.12.93 tar.gz true --disable-docs
}
##### ICONV #####
@@ -588,8 +588,7 @@ function make_glib {
make_gettext
make_libffi
make_libpcre
- # build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.46 glib-2.46.0 tar.xz true
- build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.47 glib-2.47.5 tar.xz true
+ build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.57 glib-2.57.1 tar.xz true
}
##### ATK #####
@@ -597,7 +596,7 @@ function make_glib {
function make_atk {
make_gettext
make_glib
- build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.18 atk-2.18.0 tar.xz true
+ build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.29 atk-2.29.1 tar.xz true
}
##### PIXBUF #####
@@ -610,7 +609,7 @@ function make_gdk-pixbuf {
# CONFIGURE PARAMETERS
# --with-included-loaders=yes statically links the image file format handlers
# This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory"
- build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32 gdk-pixbuf-2.32.1 tar.xz true --with-included-loaders=yes
+ build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.36 gdk-pixbuf-2.36.12 tar.xz true --with-included-loaders=yes
}
##### CAIRO #####
@@ -621,7 +620,7 @@ function make_cairo {
make_glib
make_pixman
make_fontconfig
- build_conf_make_inst http://cairographics.org/releases cairo-1.14.2 tar.xz true
+ build_conf_make_inst http://cairographics.org/releases rcairo-1.15.13 tar.xz true
}
##### PANGO #####
@@ -630,7 +629,7 @@ function make_pango {
make_cairo
make_glib
make_fontconfig
- build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.38 pango-1.38.0 tar.xz true
+ build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.42 pango-1.42.1 tar.xz true
}
##### GTK2 #####
@@ -647,7 +646,7 @@ function make_gtk2 {
make_pango
make_gdk-pixbuf
make_cairo
- build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24 gtk+-2.24.28 tar.xz patch_gtk2
+ build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24 gtk+-2.24.32 tar.xz patch_gtk2
fi
}
@@ -660,7 +659,7 @@ function make_gtk3 {
make_gdk-pixbuf
make_cairo
make_libepoxy
- build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.16 gtk+-3.16.7 tar.xz true
+ build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.22 gtk+-3.22.30 tar.xz true
# make all incl. tests and examples runs through fine
# make install fails with issue with
@@ -740,7 +739,7 @@ function install_flexlink {
# An alternative is to first build an OCaml without shared library support and build flexlink with it
function get_flex_dll_link_bin {
- if build_prep http://alain.frisch.fr/flexdll flexdll-bin-0.34 zip 1 ; then
+ if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip 1 ; then
install_flexdll
install_flexlink
build_post
@@ -750,7 +749,7 @@ function get_flex_dll_link_bin {
# Build flexdll and flexlink from sources after building OCaml
function make_flex_dll_link {
- if build_prep http://alain.frisch.fr/flexdll flexdll-0.34 tar.gz ; then
+ if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip ; then
if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
# shellcheck disable=SC2086
log1 make $MAKE_OPT build_mingw flexlink.exe
@@ -791,11 +790,10 @@ function make_ln {
function make_ocaml {
get_flex_dll_link_bin
- if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.02 ocaml-4.02.3 tar.gz 1 ; then
- # if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.01 ocaml-4.01.0 tar.gz 1 ; then
- # See README.win32
- cp config/m-nt.h config/m.h
- cp config/s-nt.h config/s.h
+ if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.06 ocaml-4.06.1 tar.gz 1 ; then
+ # See README.win32.adoc
+ cp config/m-nt.h byterun/caml/m.h
+ cp config/s-nt.h byterun/caml/s.h
if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
cp config/Makefile.mingw config/Makefile
elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
@@ -831,9 +829,9 @@ function make_ocaml {
# 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources.
rm -f ./*.txt
cp LICENSE "$PREFIXOCAML/license_readme/ocaml/License.txt"
- cp INSTALL "$PREFIXOCAML/license_readme/ocaml/Install.txt"
- cp README "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt"
- cp README.win32 "$PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt"
+ cp INSTALL.adoc "$PREFIXOCAML/license_readme/ocaml/Install.txt"
+ cp README.adoc "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt"
+ cp README.win32.adoc "$PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt"
cp VERSION "$PREFIXOCAML/license_readme/ocaml/Version.txt"
cp Changes "$PREFIXOCAML/license_readme/ocaml/Changes.txt"
fi
@@ -854,16 +852,30 @@ function make_ocaml_tools {
##### OCAML EXTRA LIBRARIES #####
function make_ocaml_libs {
+ make_num
make_findlib
make_lablgtk
# make_stdint
}
+##### Ocaml num library #####
+function make_num {
+ make_ocaml
+ # We need this commit due to windows fixed, IMHO this is better than patching v1.1.
+ if build_prep https://github.com/ocaml/num/archive/ 7dd5e935aaa2b902585b3b2d0e55ad9b2442fff0 zip 1 num-1.1-7d; then
+ log2 make all
+ # log2 make test
+ log2 make install
+ log2 make clean
+ build_post
+ fi
+}
+
##### FINDLIB Ocaml library manager #####
function make_findlib {
make_ocaml
- if build_prep https://opam.ocaml.org/archives ocamlfind.1.5.6+opam tar.gz 1 ; then
+ if build_prep https://opam.ocaml.org/archives ocamlfind.1.8.0+opam tar.gz 1 ; then
logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf"
# Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
log2 make all
@@ -900,7 +912,7 @@ function make_camlp4 {
if ! command camlp4 ; then
make_ocaml
make_findlib
- if build_prep https://github.com/ocaml/camlp4/archive 4.02+6 tar.gz 1 camlp4-4.02+6 ; then
+ if build_prep https://github.com/ocaml/camlp4/archive 4.06+2 tar.gz 1 camlp4-4.06+2 ; then
# See https://github.com/ocaml/camlp4/issues/41#issuecomment-112018910
logn configure ./configure
# Note: camlp4 doesn't support -j 8, so don't pass MAKE_OPT
@@ -917,7 +929,8 @@ function make_camlp4 {
function make_camlp5 {
make_ocaml
make_findlib
- if build_prep http://camlp5.gforge.inria.fr/distrib/src camlp5-6.14 tgz 1 ; then
+
+ if build_prep https://github.com/camlp5/camlp5/archive rel705 tar.gz 1 camlp5-rel705; then
logn configure ./configure
# Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
@@ -944,10 +957,10 @@ function make_camlp5 {
function make_lablgtk {
make_ocaml
make_findlib
- make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5
+ # make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5
make_gtk2
make_gtk_sourceview2
- if build_prep https://forge.ocamlcore.org/frs/download.php/1479 lablgtk-2.18.3 tar.gz 1 ; then
+ if build_prep https://forge.ocamlcore.org/frs/download.php/1726 lablgtk-2.18.6 tar.gz 1 ; then
# configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe
logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML"
@@ -1130,8 +1143,10 @@ function copy_coq_license {
function make_coq {
make_ocaml
- make_lablgtk
+ make_num
+ make_findlib
make_camlp5
+ make_lablgtk
if
case $COQ_VERSION in
# e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip
diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch b/dev/build/windows/patches_coq/lablgtk-2.18.6.patch
new file mode 100644
index 000000000..23c303135
--- /dev/null
+++ b/dev/build/windows/patches_coq/lablgtk-2.18.6.patch
@@ -0,0 +1,101 @@
+diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with:
+difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1
+TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz
+FOLDER= lablgtk-2.18.3
+TARSTRIP= 1
+TARPREFIX= lablgtk-2.18.3/
+ORIGFOLDER= lablgtk-2.18.3.orig
+--- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100
++++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200
+@@ -2667,7 +2667,7 @@
+ fi
+
+
+-if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then
++if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then
+ { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5
+ $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;}
+ OCAMLFIND=no
+--- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200
+@@ -75,6 +75,7 @@
+ type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
+ type id
+ val channel_of_descr : Unix.file_descr -> channel
++ val channel_of_descr_socket : Unix.file_descr -> channel
+ val add_watch :
+ cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+ val remove : id -> unit
+--- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200
+@@ -72,6 +72,8 @@
+ type id
+ external channel_of_descr : Unix.file_descr -> channel
+ = "ml_g_io_channel_unix_new"
++ external channel_of_descr_socket : Unix.file_descr -> channel
++ = "ml_g_io_channel_unix_new_socket"
+ external remove : id -> unit = "ml_g_source_remove"
+ external add_watch :
+ cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+--- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200
+@@ -461,9 +461,9 @@
+ do rm -f "$(BINDIR)"/$$f; done
+
+ lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS)
+- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
+ lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx)
+- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
+ lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS)
+
+ lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS)
+--- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200
+@@ -25,6 +25,8 @@
+ #include <string.h>
+ #include <locale.h>
+ #ifdef _WIN32
++/* to kill a #warning: include winsock2.h before windows.h */
++#include <winsock2.h>
+ #include "win32.h"
+ #include <wtypes.h>
+ #include <io.h>
+@@ -38,6 +40,11 @@
+ #include <caml/callback.h>
+ #include <caml/threads.h>
+
++#ifdef _WIN32
++/* for Socket_val */
++#include <caml/unixsupport.h>
++#endif
++
+ #include "wrappers.h"
+ #include "ml_glib.h"
+ #include "glib_tags.h"
+@@ -325,14 +332,23 @@
+
+ #ifndef _WIN32
+ ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
++CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) {
++ return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1)));
++}
+
+ #else
+ CAMLprim value ml_g_io_channel_unix_new(value wh)
+ {
+ return Val_GIOChannel_noref
+- (g_io_channel_unix_new
++ (g_io_channel_win32_new_fd
+ (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY)));
+ }
++
++CAMLprim value ml_g_io_channel_unix_new_socket(value wh)
++{
++ return Val_GIOChannel_noref
++ (g_io_channel_win32_new_socket(Socket_val(wh)));
++}
+ #endif
+
+ static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c,
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index c72705c7f..7bf9ad8c9 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -1,9 +1,15 @@
#!/bin/bash
+
set -e -x
+
+APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c
+
wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz
tar -xf opam64.tar.xz
bash opam64/install.sh
-opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
+
+opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH
eval "$(opam config env)"
-opam install -y ocamlfind camlp5 ounit
+opam install -y num ocamlfind camlp5 ounit
+
cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5c882ee85..87d837b38 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -170,3 +170,15 @@
########################################################################
: "${pidetop_CI_BRANCH:=v8.9}"
: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}"
+
+########################################################################
+# ext-lib
+########################################################################
+: "${ext_lib_CI_BRANCH:=master}"
+: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}"
+
+########################################################################
+# quickchick
+########################################################################
+: "${quickchick_CI_BRANCH:=master}"
+: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.git}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f867fd189..5b5cbd11a 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,6 +8,7 @@ export NJOBS
if [ -n "${GITLAB_CI}" ];
then
+ export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH"
export COQBIN="$PWD/_install_ci/bin"
export CI_BRANCH="$CI_COMMIT_REF_NAME"
if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
@@ -27,6 +28,7 @@ else
CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
export CI_BRANCH
fi
+ export OCAMLPATH="$PWD:$OCAMLPATH"
export COQBIN="$PWD/bin"
fi
export PATH="$COQBIN:$PATH"
diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh
new file mode 100755
index 000000000..cf212c2fb
--- /dev/null
+++ b/dev/ci/ci-ext-lib.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}" ];
+then
+ . "${ci_dir}/ci-common.sh"
+fi
+
+ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib"
+
+git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}"
+
+( cd "${ext_lib_CI_DIR}" && make && make install)
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index 2ac4d2167..32cba0808 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -12,13 +12,11 @@ git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
# `-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
-( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install )
+( cd "${pidetop_CI_DIR}" && 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/ci-quickchick.sh b/dev/ci/ci-quickchick.sh
new file mode 100755
index 000000000..fc39e2685
--- /dev/null
+++ b/dev/ci/ci-quickchick.sh
@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}" ];
+then
+ . "${ci_dir}/ci-common.sh"
+fi
+
+quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick"
+
+install_ssreflect
+
+git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}"
+
+( cd "${quickchick_CI_DIR}" && make && make install)
diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
new file mode 100644
index 000000000..115f29f1e
--- /dev/null
+++ b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
@@ -0,0 +1,14 @@
+if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then
+
+ _OVERLAY_BRANCH=vernac+move_parser
+
+ Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ ltac2_CI_BRANCH="$_OVERLAY_BRANCH"
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index cd28b1b50..4838dd734 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -4,7 +4,7 @@
Misctypes
- Syntax for universe sorts and kinds has been moved from `Misctypes`
+- Syntax for universe sorts and kinds has been moved from `Misctypes`
to `Glob_term`, as these are turned into kernel terms by
`Pretyping`.
@@ -41,6 +41,25 @@ Printer.ml API
pr_subgoal and pr_goal was removed to simplify the code. It was
earlierly used by PCoq.
+Source code organization
+
+- We have eliminated / fused some redundant modules and relocated a
+ few interfaces files. The `intf` folder is gone, and now for example
+ `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and
+ so on. Changes should be compatible, but in a few cases stricter
+ layering requirements may mean that functions have moved. In all
+ cases adapting is a matter of changing the module name.
+
+Vernacular commands
+
+- The implementation of vernacular commands has been refactored so it
+ is self-contained now, including the parsing and extension
+ mechanisms. This involves a couple of non-backward compatible
+ changes due to layering issues, where some functions have been moved
+ from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in
+ `tactics/`. In all cases adapting is a matter of changing the module
+ name.
+
### Unit testing
The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 2ddf927d9..16917586f 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,5 +1,6 @@
open Format
open Term
+open Constr
open Names
open Cbytecodes
open Cemitcodes
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 08:44:36 +0000