aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-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/README.md5
-rw-r--r--dev/ci/appveyor.sh10
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile37
-rw-r--r--dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh4
-rw-r--r--dev/ci/user-overlays/07495-gares-elpi-test-bug.sh8
-rw-r--r--dev/doc/changes.md4
-rw-r--r--dev/doc/primproj.md41
-rw-r--r--dev/doc/universes.md (renamed from dev/doc/univpoly.txt)191
-rw-r--r--dev/doc/universes.txt26
11 files changed, 304 insertions, 194 deletions
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/README.md b/dev/ci/README.md
index 697a160ca..dc586c61f 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -89,6 +89,11 @@ We are currently running tests on the following platforms:
- AppVeyor is used to test the compilation of Coq and run the test-suite on
Windows.
+GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit
+message to bypass CI. Do not use this unless your commit only changes files
+that are not compiled (e.g. Markdown files like this one, or files under
+[`.github/`](/.github/)).
+
You can anticipate the results of most of these tests prior to submitting your
PR by running GitLab CI on your private branches. To do so follow these steps:
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/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index a1178ee2a..1a83593f5 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-05-07-V2"
+# CACHEKEY: "bionic_coq-V2018-06-04-V2"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -8,7 +8,7 @@ ENV DEBIAN_FRONTEND="noninteractive"
RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \
libgtk2.0-dev libgtksourceview2.0-dev \
- texlive-latex-extra texlive-fonts-recommended hevea \
+ texlive-latex-extra texlive-fonts-recommended texlive-science \
python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip
RUN pip3 install antlr4-python3-runtime
@@ -19,15 +19,19 @@ ENV NJOBS="2" \
OPAMROOTISOK="true"
# Base opam is the set of base packages required by Coq
-ENV COMPILER="4.02.3" \
- BASE_OPAM="num ocamlfind jbuilder ounit"
+ENV COMPILER="4.02.3"
RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update
-# Setup of the base switch; CI_OPAM contains Coq's CI dependencies.
+# Common OPAM packages.
+# `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 jbuilder.1.0+beta20 ounit.2.0.8" \
+ CI_OPAM="menhir.20180530 elpi.1.0.3 ocamlgraph.1.8.8"
+
+# BASE switch; CI_OPAM contains Coq's CI dependencies.
ENV CAMLP5_VER="6.14" \
- COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" \
- CI_OPAM="menhir elpi ocamlgraph"
+ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \
opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
@@ -36,14 +40,15 @@ RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \
RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER
-# BE switch
-ENV COMPILER_BE="4.06.1" \
- CAMLP5_VER_BE="7.05" \
- COQIDE_OPAM_BE="lablgtk.2.18.6 conf-gtksourceview.2"
+# EDGE switch
+ENV COMPILER_EDGE="4.06.1" \
+ CAMLP5_VER_EDGE="7.05" \
+ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2"
-RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \
- opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE
+RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \
+ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
-# BE+flambda switch
-RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \
- opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE $CI_OPAM
+# EDGE+flambda switch, we install CI_OPAM as to be able to use
+# `ci-template-flambda` with everything.
+RUN opam switch -y -j $NJOBS "${COMPILER_EDGE}+flambda" && eval $(opam config env) && \
+ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh
new file mode 100644
index 000000000..e6c48d10a
--- /dev/null
+++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then
+ Equations_CI_BRANCH=unification-returns-option
+ Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh
new file mode 100644
index 000000000..6939ead2b
--- /dev/null
+++ b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then
+
+ # this branch contains a commit not present on coq-master that triggers
+ # the universe restriction bug #7472
+ Elpi_CI_BRANCH=overlay-7495
+ Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 4838dd734..bb8189efc 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -28,6 +28,10 @@ Proof engine
should indicate what the canonical form is. An important change is
the move of `Globnames.global_reference` to `Names.GlobRef.t`.
+- Unification API returns `evar_map option` instead of `bool * evar_map`
+ with the guarantee that the `evar_map` was unchanged if the boolean
+ was false.
+
ML Libraries used by Coq
- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
diff --git a/dev/doc/primproj.md b/dev/doc/primproj.md
new file mode 100644
index 000000000..ea76aeeab
--- /dev/null
+++ b/dev/doc/primproj.md
@@ -0,0 +1,41 @@
+Primitive Projections
+---------------------
+
+ | Proj of Projection.t * constr
+
+Projections are always applied to a term, which must be of a record
+type (i.e. reducible to an inductive type `I params`). Type-checking,
+reduction and conversion are fast (not as fast as they could be yet)
+because we don't keep parameters around. As you can see, it's
+currently a `constant` that is used here to refer to the projection,
+that will change to an abstract `projection` type in the future.
+Basically a projection constant records which inductive it is a
+projection for, the number of params and the actual position in the
+constructor that must be projected. For compatibility reason, we also
+define an eta-expanded form (accessible from user syntax `@f`). The
+constant_entry of a projection has both informations. Declaring a
+record (under `Set Primitive Projections`) will generate such
+definitions. The API to declare them is not stable at the moment, but
+the inductive type declaration also knows about the projections, i.e.
+a record inductive type decl contains an array of terms representing
+the projections. This is used to implement eta-conversion for record
+types (with at least one field and having all projections definable).
+The canonical value being `Build_R (pn x) ... (pn x)`. Unification and
+conversion work up to this eta rule. The records can also be universe
+polymorphic of course, and we don't need to keep track of the universe
+instance for the projections either. Projections are reduced _eagerly_
+everywhere, and introduce a new `Zproj` constructor in the abstract
+machines that obeys both the delta (for the constant opacity) and iota
+laws (for the actual reduction). Refolding works as well (afaict), but
+there is a slight hack there related to universes (not projections).
+
+For the ML programmer, the biggest change is that pattern-matchings on
+kind_of_term require an additional case, that is handled usually
+exactly like an `App (Const p) arg`.
+
+There are slight hacks related to hints is well, to use the primitive
+projection form of f when one does `Hint Resolve f`. Usually hint
+resolve will typecheck the term, resulting in a partially applied
+projection (disallowed), so we allow it to take
+`constr_or_global_reference` arguments instead and special-case on
+projections. Other tactic extensions might need similar treatment.
diff --git a/dev/doc/univpoly.txt b/dev/doc/universes.md
index ca3d520c7..c276603ed 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/universes.md
@@ -1,11 +1,11 @@
-Notes on universe polymorphism and primitive projections, M. Sozeau
-===================================================================
+Notes on universe polymorphism
+------------------------------
-The new implementation of universe polymorphism and primitive
-projections introduces a few changes to the API of Coq. First and
-foremost, the term language changes, as global references now carry a
-universe level substitution:
+The implementation of universe polymorphism introduces a few changes
+to the API of Coq. First and foremost, the term language changes, as
+global references now carry a universe level substitution:
+~~~ocaml
type 'a puniverses = 'a * Univ.Instance.t
type pconstant = constant puniverses
type pinductive = inductive puniverses
@@ -15,30 +15,31 @@ type constr = ...
| Const of puniverses
| Ind of pinductive
| Constr of pconstructor
- | Proj of constant * constr
-
+~~~
Universes
-=========
+---------
- Universe instances (an array of levels) gets substituted when
+Universe instances (an array of levels) gets substituted when
unfolding definitions, are used to typecheck and are unified according
-to the rules in the ITP'14 paper on universe polymorphism in Coq.
+to the rules in the ITP'14 paper on universe polymorphism in Coq.
+~~~ocaml
type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *)
type Instance.t = Level.t array
type Universe.t = Level.t list (* hashconsed *)
+~~~
The universe module defines modules and abstract types for levels,
universes etc.. Structures are hashconsed (with a hack to take care
-of the fact that deserialization breaks sharing).
+of the fact that deserialization breaks sharing).
- Definitions (constants, inductives) now carry around not only
+ Definitions (constants, inductives) now carry around not only
constraints but also the universes they introduced (a Univ.UContext.t).
-There is another kind of contexts [Univ.ContextSet.t], the latter has
+There is another kind of contexts `Univ.ContextSet.t`, the latter has
a set of universes, while the former has serialized the levels in an
-array, and is used for polymorphic objects. Both have "reified"
-constraints depending on global and local universes.
+array, and is used for polymorphic objects. Both have "reified"
+constraints depending on global and local universes.
A polymorphic definition is abstract w.r.t. the variables in this
context, while a monomorphic one (or template polymorphic) just adds the
@@ -46,18 +47,18 @@ universes and constraints to the global universe context when it is put
in the environment. No other universes than the global ones and the
declared local ones are needed to check a declaration, hence the kernel
does not produce any constraints anymore, apart from module
-subtyping.... There are hence two conversion functions now: [check_conv]
-and [infer_conv]: the former just checks the definition in the current env
+subtyping.... There are hence two conversion functions now: `check_conv`
+and `infer_conv`: the former just checks the definition in the current env
(in which we usually push_universe_context of the associated context),
-and [infer_conv] which produces constraints that were not implied by the
+and `infer_conv` which produces constraints that were not implied by the
ambient constraints. Ideally, that one could be put out of the kernel,
-but currently module subtyping needs it.
+but currently module subtyping needs it.
Inference of universes is now done during refinement, and the evar_map
carries the incrementally built universe context, starting from the
-global universe constraints (see [Evd.from_env]). [Evd.conversion] is a
-wrapper around [infer_conv] that will do the bookkeeping for you, it
-uses [evar_conv_x]. There is a universe substitution being built
+global universe constraints (see `Evd.from_env`). `Evd.conversion` is a
+wrapper around `infer_conv` that will do the bookkeeping for you, it
+uses `evar_conv_x`. There is a universe substitution being built
incrementally according to the constraints, so one should normalize at
the end of a proof (or during a proof) with that substitution just like
we normalize evars. There are some nf_* functions in
@@ -67,16 +68,16 @@ the universe constraints used in the term. It is heuristic but
validity-preserving. No user-introduced universe (i.e. coming from a
user-written anonymous Type) gets touched by this, only the fresh
universes generated for each global application. Using
-
+~~~ocaml
val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
-
+~~~
Is the way to make a constr out of a global reference in the new API.
If they constr is polymorphic, it will add the necessary constraints to
the evar_map. Even if a constr is not polymorphic, we have to take care
of keeping track of its universes. Typically, using:
-
- mkApp (coq_id_function, [| A; a |])
-
+~~~ocaml
+ mkApp (coq_id_function, [| A; a |])
+~~~
and putting it in a proof term is not enough now. One has to somehow
show that A's type is in cumululativity relation with id's type
argument, incurring a universe constraint. To do this, one can simply
@@ -84,19 +85,19 @@ call Typing.resolve_evars env evdref c which will do some infer_conv to
produce the right constraints and put them in the evar_map. Of course in
some cases you might know from an invariant that no new constraint would
be produced and get rid of it. Anyway the kernel will tell you if you
-forgot some. As a temporary way out, [Universes.constr_of_global] allows
+forgot some. As a temporary way out, `Universes.constr_of_global` allows
you to make a constr from any non-polymorphic constant, but it will fail
on polymorphic ones.
Other than that, unification (w_unify and evarconv) now take account of universes and
produce only well-typed evar_maps.
-Some syntactic comparisons like the one used in [change] have to be
-adapted to allow identification up-to-universes (when dealing with
-polymorphic references), [make_eq_univs_test] is there to help.
+Some syntactic comparisons like the one used in `change` have to be
+adapted to allow identification up-to-universes (when dealing with
+polymorphic references), `make_eq_univs_test` is there to help.
In constr, there are actually many new comparison functions to deal with
that:
-
+~~~ocaml
(** [equal a b] is true if [a] equals [b] modulo alpha, casts,
and application grouping *)
val equal : constr -> constr -> bool
@@ -105,7 +106,7 @@ val equal : constr -> constr -> bool
application grouping and the universe equalities in [u]. *)
val eq_constr_univs : constr Univ.check_function
-(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
alpha, casts, application grouping and the universe inequalities in [u]. *)
val leq_constr_univs : constr Univ.check_function
@@ -120,47 +121,47 @@ val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained
(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
application grouping and ignoring universe instances. *)
val eq_constr_nounivs : constr -> constr -> bool
-
-The [_univs] versions are doing checking of universe constraints
-according to a graph, while the [_universes] are producing (non-atomic)
+~~~
+The `_univs` versions are doing checking of universe constraints
+according to a graph, while the `_universes` are producing (non-atomic)
universe constraints. The non-atomic universe constraints include the
-[ULub] constructor: when comparing [f (* u1 u2 *) c] and [f (* u1' u2'
-*) c] we add ULub constraints on [u1, u1'] and [u2, u2']. These are
-treated specially: as unfolding [f] might not result in these
+`ULub` constructor: when comparing `f (* u1 u2 *) c` and `f (* u1' u2'
+*) c` we add ULub constraints on `u1, u1'` and `u2, u2'`. These are
+treated specially: as unfolding `f` might not result in these
unifications, we need to keep track of the fact that failure to satisfy
them does not mean that the term are actually equal. This is used in
-unification but probably not necessary to the average programmer.
+unification but probably not necessary to the average programmer.
Another issue for ML programmers is that tables of constrs now usually
-need to take a [constr Univ.in_universe_context_set] instead, and
-properly refresh the universes context when using the constr, e.g. using
-Clenv.refresh_undefined_univs clenv or:
-
+need to take a `constr Univ.in_universe_context_set` instead, and
+properly refresh the universes context when using the constr, e.g. using
+Clenv.refresh_undefined_univs clenv or:
+~~~ocaml
(** Get fresh variables for the universe context.
Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : universe_context_set ->
+val fresh_universe_context_set_instance : universe_context_set ->
universe_level_subst * universe_context_set
-
-The substitution should be applied to the constr(s) under consideration,
+~~~
+The substitution should be applied to the constr(s) under consideration,
and the context_set merged with the current evar_map with:
-
+~~~ocaml
val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
-
-The [rigid] flag here should be [Evd.univ_flexible] most of the
+~~~
+The `rigid` flag here should be `Evd.univ_flexible` most of the
time. This means the universe levels of polymorphic objects in the
-constr might get instantiated instead of generating equality constraints
+constr might get instantiated instead of generating equality constraints
(Evd.univ_rigid does that).
-On this issue, I recommend forcing commands to take [global_reference]s
+On this issue, I recommend forcing commands to take `global_reference`s
only, the user can declare his specialized terms used as hints as
constants and this is cleaner. Alas, backward-compatibility-wise,
this is the only solution I found. In the case of global_references
-only, it's just a matter of using [Evd.fresh_global] /
-[pf_constr_of_global] to let the system take care of universes.
+only, it's just a matter of using `Evd.fresh_global` /
+`pf_constr_of_global` to let the system take care of universes.
The universe graph
-==================
+------------------
To accomodate universe polymorphic definitions, the graph structure in
kernel/univ.ml was modified. The new API forces every universe to be
@@ -176,68 +177,14 @@ no universe i can be set lower than Set, so the chain of universes
always bottoms down at Prop < Set.
Modules
-=======
+-------
One has to think of universes in modules as being globally declared, so
when including a module (type) which declares a type i (e.g. through a
parameter), we get back a copy of i and not some fresh universe.
-Projections
-===========
-
- | Proj of constant * constr
-
-Projections are always applied to a term, which must be of a record type
-(i.e. reducible to an inductive type [I params]). Type-checking,
-reduction and conversion are fast (not as fast as they could be yet)
-because we don't keep parameters around. As you can see, it's currently
-a [constant] that is used here to refer to the projection, that will
-change to an abstract [projection] type in the future. Basically a
-projection constant records which inductive it is a projection for, the
-number of params and the actual position in the constructor that must be
-projected. For compatibility reason, we also define an eta-expanded form
-(accessible from user syntax @f). The constant_entry of a projection has
-both informations. Declaring a record (under [Set Primitive
-Projections]) will generate such definitions. The API to declare them is
-not stable at the moment, but the inductive type declaration also knows
-about the projections, i.e. a record inductive type decl contains an
-array of terms representing the projections. This is used to implement
-eta-conversion for record types (with at least one field and having all
-projections definable). The canonical value being [Build_R (pn x)
-... (pn x)]. Unification and conversion work up to this eta rule. The
-records can also be universe polymorphic of course, and we don't need to
-keep track of the universe instance for the projections either.
-Projections are reduced _eagerly_ everywhere, and introduce a new Zproj
-constructor in the abstract machines that obeys both the delta (for the
-constant opacity) and iota laws (for the actual reduction). Refolding
-works as well (afaict), but there is a slight hack there related to
-universes (not projections).
-
-For the ML programmer, the biggest change is that pattern-matchings on
-kind_of_term require an additional case, that is handled usually exactly
-like an [App (Const p) arg].
-
-There are slight hacks related to hints is well, to use the primitive
-projection form of f when one does [Hint Resolve f]. Usually hint
-resolve will typecheck the term, resulting in a partially applied
-projection (disallowed), so we allow it to take
-[constr_or_global_reference] arguments instead and special-case on
-projections. Other tactic extensions might need similar treatment.
-
-WIP
-===
-
-- [vm_compute] does not deal with universes and projections correctly,
-except when it goes to a normal form with no projections or polymorphic
-constants left (the most common case). E.g. Ring with Set Universe
-Polymorphism and Set Primitive Projections work (at least it did at some
-point, I didn't recheck yet).
-
-- [native_compute] works with universes and projections.
-
-
Incompatibilities
-=================
+-----------------
Old-style universe polymorphic definitions were implemented by taking
advantage of the fact that elaboration (i.e., pretyping and unification)
@@ -247,33 +194,33 @@ possible, as unification ensures that the substitution is built is
entirely well-typed, even w.r.t universes. This means that some terms
that type-checked before no longer do, especially projections of the
pair:
-
+~~~coq
@fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)).
-
+~~~
The "template universe polymorphic" variables i and j appear during
typing without being refreshed, meaning that they can be lowered (have
upper constraints) with user-introduced universes. In most cases this
won't work, so ?x and ?y have to be instantiated earlier, either from
the type of the actual projected pair term (some t : prod A B) or the
-typing constraint. Adding the correct type annotations will always fix
+typing constraint. Adding the correct type annotations will always fix
this.
Unification semantics
-=====================
+---------------------
In Ltac, matching with:
-- a universe polymorphic constant [c] matches any instance of the
+- a universe polymorphic constant `c` matches any instance of the
constant.
-- a variable ?x already bound to a term [t] (non-linear pattern) uses
+- a variable ?x already bound to a term `t` (non-linear pattern) uses
strict equality of universes (e.g., Type@{i} and Type@{j} are not
equal).
In tactics:
-- [change foo with bar], [pattern foo] will unify all instances of [foo]
- (and convert them with [bar]). This might incur unifications of
- universes. [change] uses conversion while [pattern] only does
+- `change foo with bar`, `pattern foo` will unify all instances of `foo`
+ (and convert them with `bar`). This might incur unifications of
+ universes. `change` uses conversion while `pattern` only does
syntactic matching up-to unification of universes.
-- [apply], [refine] use unification up to universes.
+- `apply`, `refine` use unification up to universes.
diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt
deleted file mode 100644
index a40706e99..000000000
--- a/dev/doc/universes.txt
+++ /dev/null
@@ -1,26 +0,0 @@
-How to debug universes?
-
-1. There is a command Print Universes in Coq toplevel
-
- Print Universes.
- prints the graph of universes in the form of constraints
-
- Print Universes "file".
- produces the "file" containing universe constraints in the form
- univ1 # univ2 ;
- where # can be either > >= or =
-
- If "file" ends with .gv or .dot, the resulting file will be in
- dot format.
-
-
- *) for dot see http://www.research.att.com/sw/tools/graphviz/
-
-
-2. There is a printing option
-
- {Set,Unset} Printing Universes.
-
- which, when set, makes all pretty-printed Type's annotated with the
- name of the universe.
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 19:42:40 +0000