diff options
Diffstat (limited to 'dev')
38 files changed, 388 insertions, 830 deletions
diff --git a/dev/README.md b/dev/README.md index d9fdd230d3..9761f7b96f 100644 --- a/dev/README.md +++ b/dev/README.md @@ -25,7 +25,6 @@ | [`dev/doc/universes.txt`](doc/universes.txt) | Help for debugging universes | | [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND | | [`dev/doc/perf-analysis`](doc/perf-analysis)| Analysis of perfs measured on the compilation of user contribs | -| [`dev/doc/cic.dtd`](doc/cic.dtd) | Official dtd of the calc. of ind. constr. for im/ex-portation | | [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | | [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | | [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 8489bcfc3a..c3f3a97ff5 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -331,7 +331,7 @@ IF "%CYGWIN_QUIET%" == "Y" ( )
IF "%GTK_FROM_SOURCES%"=="N" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+ SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk3,mingw64-%ARCH%-gtksourceview3.0
)
REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
@@ -373,7 +373,8 @@ IF "%RUNSETUP%"=="Y" ( -P make,unzip ^
-P gdb,liblzma5 ^
-P patch,automake1.14 ^
- -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
+ -P pkg-config ^
+ -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-windows_default_manifest ^
-P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
-P libiconv-devel,libunistring-devel,libncurses-devel ^
-P gettext-devel,libgettextpo-devel ^
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 2e934ff0c0..4c5bd29236 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -742,7 +742,7 @@ function make_fontconfig { ##### ICONV ##### function make_libiconv { - build_conf_make_inst http://ftp.gnu.org/pub/gnu/libiconv libiconv-1.14 tar.gz true + build_conf_make_inst http://ftp.gnu.org/pub/gnu/libiconv libiconv-1.15 tar.gz true } ##### UNISTRING ##### @@ -816,7 +816,9 @@ function make_glib { make_gettext make_libffi make_libpcre + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.57 glib-2.57.1 tar.xz true + } ##### ATK ##### @@ -824,7 +826,7 @@ function make_glib { function make_atk { make_gettext make_glib - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.29 atk-2.29.1 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.30 atk-2.30.0 tar.xz true } ##### PIXBUF ##### @@ -837,7 +839,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.36 gdk-pixbuf-2.36.12 tar.xz true --with-included-loaders=yes + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.38 gdk-pixbuf-2.38.0 tar.xz true --with-included-loaders=yes } ##### CAIRO ##### @@ -848,7 +850,7 @@ function make_cairo { make_glib make_pixman make_fontconfig - build_conf_make_inst http://cairographics.org/releases rcairo-1.15.13 tar.xz true + build_conf_make_inst http://cairographics.org/releases rcairo-1.16.2 tar.xz true } ##### PANGO ##### @@ -857,37 +859,23 @@ function make_pango { make_cairo make_glib make_fontconfig - build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.42 pango-1.42.1 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.42 pango-1.42.4 tar.xz true } -##### GTK2 ##### +##### GTK3 ##### -function patch_gtk2 { - rm gtk/gtk.def -} +function make_gtk3 { -function make_gtk2 { - # Cygwin packet dependencies: gtk-update-icon-cache if [ "$GTK_FROM_SOURCES" == "Y" ]; then - make_glib - make_atk - make_pango - make_gdk-pixbuf - make_cairo - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24 gtk+-2.24.32 tar.xz patch_gtk2 - fi -} - -##### GTK3 ##### -function make_gtk3 { - make_glib - make_atk - make_pango - make_gdk-pixbuf - make_cairo - make_libepoxy - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.22 gtk+-3.22.30 tar.xz true + make_glib + make_atk + make_pango + make_gdk-pixbuf + make_cairo + make_libepoxy + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.24 gtk+-3.24.5 tar.xz true + fi # make all incl. tests and examples runs through fine # make install fails with issue with @@ -918,17 +906,17 @@ function make_libxml2 { fi } -##### GTK-SOURCEVIEW2 ##### +##### GTK-SOURCEVIEW3 ##### -function make_gtk_sourceview2 { +function make_gtk_sourceview3 { # Cygwin packet dependencies: intltool # gtksourceview-2.11.2 requires GTK2 # gtksourceview-2.91.9 requires GTK3 # => We use gtksourceview-2.11.2 which seems to be the newest GTK2 based one if [ "$GTK_FROM_SOURCES" == "Y" ]; then - make_gtk2 + make_gtk3 make_libxml2 - build_conf_make_inst https://download.gnome.org/sources/gtksourceview/2.11 gtksourceview-2.11.2 tar.bz2 true + build_conf_make_inst https://download.gnome.org/sources/gtksourceview/3.24 gtksourceview-3.24.9 tar.bz2 true fi } @@ -977,7 +965,7 @@ function get_flex_dll_link_bin { # Build flexdll and flexlink from sources after building OCaml function make_flex_dll_link { - if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip ; then + if build_prep https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 ; then if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then # shellcheck disable=SC2086 log1 make $MAKE_OPT build_mingw flexlink.exe @@ -1014,11 +1002,21 @@ function make_ln { fi } +##### ARCH-pkg-config replacement ##### + +# cygwin replaced ARCH-pkg-config with a shell script, which doesn't work e.g. for dune on Windows. +# This builds a binary replacement for the shell script and puts it into the bin_special folder. +# There is no global installation since it is module specific what pkg-config is needed under what name. + +function make_arch_pkg_config { + gcc -DARCH="$TARGET_ARCH" -o bin_special/pkg-config.exe $PATCHES/pkg-config.c +} + ##### OCAML ##### function make_ocaml { get_flex_dll_link_bin - if build_prep https://github.com/ocaml/ocaml/archive 4.07.0 tar.gz 1 ocaml-4.07.0 ; then + if build_prep https://github.com/ocaml/ocaml/archive 4.07.1 tar.gz 1 ocaml-4.07.1 ; then # See README.win32.adoc cp config/m-nt.h byterun/caml/m.h cp config/s-nt.h byterun/caml/s.h @@ -1073,7 +1071,6 @@ function make_ocaml { function make_ocaml_tools { make_findlib - # make_camlp5 } ##### OCAML EXTRA LIBRARIES ##### @@ -1082,7 +1079,6 @@ function make_ocaml_libs { make_num make_findlib make_lablgtk - # make_stdint } ##### Ocaml num library ##### @@ -1130,6 +1126,20 @@ function make_findlib { fi } +##### Dune build system ##### + +function make_dune { + make_ocaml + + if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 dune-1.6.3 ; then + + log2 make release + log2 make install + + build_post + fi +} + ##### MENHIR Ocaml Parser Generator ##### function make_menhir { @@ -1144,108 +1154,44 @@ function make_menhir { fi } -##### CAMLP4 Ocaml Preprocessor ##### - -function make_camlp4 { - # OCaml up to 4.01 includes camlp4, from 4.02 it isn't included - # Check if command camlp4 exists, if not build camlp4 - if ! command camlp4 ; then - make_ocaml - make_findlib - 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 - log2 make all - log2 make install - log2 make clean - build_post - fi - fi -} - -##### CAMLP5 Ocaml Preprocessor ##### - -function make_camlp5 { - make_ocaml - make_findlib - - if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; 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 - # shellcheck disable=SC2086 - log1 make world.opt $MAKE_OPT - log2 make install - # For some reason gramlib.a is not copied, but it is required by Coq - cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/" - # For some reason META is not copied, but it is required by coq_makefile - log2 make -C etc META - mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/" - cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/" - log2 make clean - build_post - fi -} - ##### LABLGTK Ocaml GTK binding ##### # Note: when rebuilding lablgtk by deleting the .finished file, # also delete <root>\usr\x86_64-w64-mingw32\sys-root\mingw\lib\site-lib # Otherwise make install fails -function make_lablgtk { - make_ocaml - make_findlib - # 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/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" - - # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT - - # lablgtk binary needs to be stripped - otherwise flexdll goes wild - # Fix version 1: explicit strip after failed build - this randomly fails in CI - # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html - # logn make-world-pre make world || true - # $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll - - # Fix version 2: Strip by passing linker argument rather than explicit call to strip - # See https://github.com/alainfrisch/flexdll/issues/6 - # Argument to ocamlmklib: -ldopt "-link -Wl,-s" - # -ldopt is the okamlmklib linker prefix option - # -link is the flexlink linker prefix option - # -Wl, is the gcc (linker driver) linker prefix option - # -s is the gnu linker option for stripping symbols - # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch - - log2 make world - - # lablgtk does not escape FINDLIBDIR path, which can contain backslashes - sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make +function make_ocaml_cairo2 { + if build_prep https://github.com/Chris00/ocaml-cairo/archive 0.6 tar.gz 1 ocaml_cairo2-0.6; then + make_arch_pkg_config - log2 make install - log2 make clean + log2 dune build cairo2.install + log2 dune install cairo2 + log2 dune clean build_post + fi } -##### Ocaml Stdint ##### - -function make_stdint { +function make_lablgtk { make_ocaml make_findlib - if build_prep https://github.com/andrenth/ocaml-stdint/archive 0.3.0 tar.gz 1 Stdint-0.3.0; then - # Note: the setup gets the proper install path from ocamlfind, but for whatever reason it wants - # to create an empty folder in some folder which defaults to C:\Program Files. - # The --preifx overrides this. Id didn't see any files created in /tmp/extra. - log_1_3 ocaml setup.ml -configure --prefix /tmp/extra - log_1_3 ocaml setup.ml -build - log_1_3 ocaml setup.ml -install - log_1_3 ocaml setup.ml -clean + make_dune + make_gtk3 + make_gtk_sourceview3 + make_ocaml_cairo2 + + if build_prep https://github.com/garrigue/lablgtk/archive 3.0.beta5 tar.gz 1 lablgtk-3.0.beta5 ; then + make_arch_pkg_config + + # lablgtk3 includes more packages that are not relevant for Coq, + # such as gtkspell + log2 dune build -p lablgtk3 + log2 dune install lablgtk3 + + log2 dune build -p lablgtk3-sourceview3 + log2 dune install lablgtk3-sourceview3 + + log2 dune clean build_post fi } @@ -1270,42 +1216,44 @@ function copy_coq_dlls { # Select all missing DLLs from the module list, right click "copy filenames" # Delay loaded DLLs from Windows can be ignored (hour-glass icon at begin of line) # Do this recursively until there are no further missing DLLs (File close + reopen) - # For running this quickly, just do "cd coq-<ver> ; call copy_coq_dlls ; cd .." at the end of this script. + # For running this quickly, just do "cd coq-<ver> ; copy_coq_dlls ; cd .." at the end of this script. # Do the same for coqc and ocamlc (usually doesn't result in additional files) - copy_coq_dll LIBATK-1.0-0.DLL copy_coq_dll LIBCAIRO-2.DLL - copy_coq_dll LIBEXPAT-1.DLL - copy_coq_dll LIBFFI-6.DLL copy_coq_dll LIBFONTCONFIG-1.DLL copy_coq_dll LIBFREETYPE-6.DLL - copy_coq_dll LIBGDK-WIN32-2.0-0.DLL + copy_coq_dll LIBGDK-3-0.DLL copy_coq_dll LIBGDK_PIXBUF-2.0-0.DLL - copy_coq_dll LIBGIO-2.0-0.DLL copy_coq_dll LIBGLIB-2.0-0.DLL - copy_coq_dll LIBGMODULE-2.0-0.DLL copy_coq_dll LIBGOBJECT-2.0-0.DLL - copy_coq_dll LIBGTK-WIN32-2.0-0.DLL - copy_coq_dll LIBINTL-8.DLL + copy_coq_dll LIBGTK-3-0.DLL + copy_coq_dll LIBGTKSOURCEVIEW-3.0-1.DLL copy_coq_dll LIBPANGO-1.0-0.DLL + copy_coq_dll LIBATK-1.0-0.DLL + copy_coq_dll LIBBZ2-1.DLL + copy_coq_dll LIBCAIRO-GOBJECT-2.DLL + copy_coq_dll LIBEPOXY-0.DLL + copy_coq_dll LIBEXPAT-1.DLL + copy_coq_dll LIBFFI-6.DLL + copy_coq_dll LIBGIO-2.0-0.DLL + copy_coq_dll LIBGMODULE-2.0-0.DLL + copy_coq_dll LIBINTL-8.DLL copy_coq_dll LIBPANGOCAIRO-1.0-0.DLL copy_coq_dll LIBPANGOWIN32-1.0-0.DLL - copy_coq_dll libpcre-1.dll + copy_coq_dll LIBPCRE-1.DLL copy_coq_dll LIBPIXMAN-1-0.DLL copy_coq_dll LIBPNG16-16.DLL copy_coq_dll LIBXML2-2.DLL copy_coq_dll ZLIB1.DLL + copy_coq_dll ICONV.DLL + copy_coq_dll LIBLZMA-5.DLL + copy_coq_dll LIBPANGOFT2-1.0-0.DLL + copy_coq_dll LIBHARFBUZZ-0.DLL # Depends on if GTK is built from sources if [ "$GTK_FROM_SOURCES" == "Y" ]; then - copy_coq_dll libiconv-2.dll - else - copy_coq_dll ICONV.DLL - copy_coq_dll LIBBZ2-1.DLL - copy_coq_dll LIBGTKSOURCEVIEW-2.0-0.DLL - copy_coq_dll LIBHARFBUZZ-0.DLL - copy_coq_dll LIBLZMA-5.DLL - copy_coq_dll LIBPANGOFT2-1.0-0.DLL + echo "Building GTK from sources is currently not supported" + exit 1 fi; # Architecture dependent files @@ -1335,14 +1283,14 @@ function copy_coq_objects { # Copy required GTK config and suport files -function copq_coq_gtk { - echo 'gtk-theme-name = "MS-Windows"' > "$PREFIX/etc/gtk-2.0/gtkrc" - echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-2.0/gtkrc" +function copy_coq_gtk { + echo 'gtk-theme-name = "Default"' > "$PREFIX/etc/gtk-3.0/gtkrc" + echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-3.0/gtkrc" if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then - install_glob "$PREFIX/etc/gtk-2.0" '*' "$PREFIXCOQ/gtk-2.0" - install_glob "$PREFIX/share/gtksourceview-2.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" - install_glob "$PREFIX/share/gtksourceview-2.0/styles" '*' "$PREFIXCOQ/share/gtksourceview-2.0/styles" + install_glob "$PREFIX/etc/gtk-3.0" '*' "$PREFIXCOQ/gtk-3.0" + install_glob "$PREFIX/share/gtksourceview-3.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-3.0/language-specs" + install_glob "$PREFIX/share/gtksourceview-3.0/styles" '*' "$PREFIXCOQ/share/gtksourceview-3.0/styles" install_rec "$PREFIX/share/themes" '*' "$PREFIXCOQ/share/themes" # This below item look like a bug in make install @@ -1351,10 +1299,7 @@ function copq_coq_gtk { else COQSHARE="$PREFIXCOQ/share/" fi - if [[ ! $COQ_VERSION == 8.4* ]] ; then - mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" - mv "$COQSHARE"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles" - fi + mkdir -p "$PREFIXCOQ/ide" mv "$COQSHARE"*.png "$PREFIXCOQ/ide" rmdir "$PREFIXCOQ/share/coq" || true @@ -1383,7 +1328,6 @@ function make_coq { make_ocaml make_num make_findlib - # make_camlp5 make_lablgtk if case $COQ_VERSION in @@ -1437,11 +1381,12 @@ function make_coq { log2 make install log1 copy_coq_dlls + log1 copy_coq_gtk + if [ "$INSTALLOCAML" == "Y" ]; then copy_coq_objects fi - log1 copq_coq_gtk log1 copy_coq_license # make clean seems to be broken for 8.5pl2 diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch index 2c8c46373f..2c8c46373f 100755..100644 --- a/dev/build/windows/patches_coq/VST.patch +++ b/dev/build/windows/patches_coq/VST.patch diff --git a/dev/build/windows/patches_coq/flexdll-0.37.patch b/dev/build/windows/patches_coq/flexdll-0.37.patch new file mode 100644 index 0000000000..82806f9ea4 --- /dev/null +++ b/dev/build/windows/patches_coq/flexdll-0.37.patch @@ -0,0 +1,19 @@ +diff/patch file created on Tue, Feb 19, 2019 9:41:26 PM with: +difftar-folder.sh tarballs/flexdll-0.37.tar.gz flexdll-0.37 1 +TARFILE= tarballs/flexdll-0.37.tar.gz +FOLDER= flexdll-0.37 +TARSTRIP= 1 +TARPREFIX= flexdll-0.37/ +ORIGFOLDER= flexdll-0.37.orig +--- flexdll-0.37.orig/cmdline.ml 2017-10-25 10:40:46.000000000 +0200 ++++ flexdll-0.37/cmdline.ml 2019-02-19 21:41:18.157024900 +0100 +@@ -248,6 +248,9 @@ + String.sub s 0 2 :: String.sub s 2 (String.length s - 2) :: tr rest + | s :: rest when String.length s >= 5 && String.sub s 0 5 = "/link" -> + "-link" :: String.sub s 5 (String.length s - 5) :: tr rest ++ (* Convert gcc linker option prefix -Wl, to flexlink linker prefix -link *) ++ | s :: rest when String.length s >= 6 && String.sub s 0 5 = "-Wl,-" -> ++ "-link" :: String.sub s 4 (String.length s - 4) :: tr rest + | "-arg" :: x :: rest -> + tr (Array.to_list (Arg.read_arg x)) @ rest + | "-arg0" :: x :: rest -> diff --git a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch b/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch deleted file mode 100644 index 73a098d12a..0000000000 --- a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch +++ /dev/null @@ -1,213 +0,0 @@ -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c 2010-05-30 12:24:14.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c 2015-10-27 14:58:54.422888400 +0100 -*************** -*** 80,86 **** - /* If string contains prefix, check that prefix is not followed - * by a unicode mark symbol, e.g. that trailing 'a' in prefix - * is not part of two-char a-with-hat symbol in string. */ -! return type != G_UNICODE_COMBINING_MARK && - type != G_UNICODE_ENCLOSING_MARK && - type != G_UNICODE_NON_SPACING_MARK; - } ---- 80,86 ---- - /* If string contains prefix, check that prefix is not followed - * by a unicode mark symbol, e.g. that trailing 'a' in prefix - * is not part of two-char a-with-hat symbol in string. */ -! return type != G_UNICODE_SPACING_MARK && - type != G_UNICODE_ENCLOSING_MARK && - type != G_UNICODE_NON_SPACING_MARK; - } -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c 2010-05-30 12:24:14.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c 2015-10-27 14:55:30.294477600 +0100 -*************** -*** 274,280 **** - * containg a list of language files directories. - * The array is owned by @lm and must not be modified. - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm) - { - g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL); ---- 274,280 ---- - * containg a list of language files directories. - * The array is owned by @lm and must not be modified. - */ -! const gchar* const * - gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm) - { - g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL); -*************** -*** 392,398 **** - * available languages or %NULL if no language is available. The array - * is owned by @lm and must not be modified. - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm) - { - g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL); ---- 392,398 ---- - * available languages or %NULL if no language is available. The array - * is owned by @lm and must not be modified. - */ -! const gchar* const * - gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm) - { - g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL); -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h 2009-11-15 00:41:33.000000000 +0100 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h 2015-10-27 14:55:30.518500000 +0100 -*************** -*** 62,74 **** - - GtkSourceLanguageManager *gtk_source_language_manager_get_default (void); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm); - - void gtk_source_language_manager_set_search_path (GtkSourceLanguageManager *lm, - gchar **dirs); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm); - - GtkSourceLanguage *gtk_source_language_manager_get_language (GtkSourceLanguageManager *lm, ---- 62,74 ---- - - GtkSourceLanguageManager *gtk_source_language_manager_get_default (void); - -! const gchar* const * - gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm); - - void gtk_source_language_manager_set_search_path (GtkSourceLanguageManager *lm, - gchar **dirs); - -! const gchar* const * - gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm); - - GtkSourceLanguage *gtk_source_language_manager_get_language (GtkSourceLanguageManager *lm, -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c 2010-05-30 12:24:14.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c 2015-10-27 14:55:30.545502700 +0100 -*************** -*** 310,316 **** - * - * Since: 2.0 - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL); ---- 310,316 ---- - * - * Since: 2.0 - */ -! const gchar* const * - gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL); -*************** -*** 318,324 **** - if (scheme->priv->authors == NULL) - return NULL; - -! return (G_CONST_RETURN gchar* G_CONST_RETURN *)scheme->priv->authors->pdata; - } - - /** ---- 318,324 ---- - if (scheme->priv->authors == NULL) - return NULL; - -! return (const gchar* const *)scheme->priv->authors->pdata; - } - - /** -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h 2010-03-29 15:02:56.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h 2015-10-27 14:55:30.565504700 +0100 -*************** -*** 61,67 **** - const gchar *gtk_source_style_scheme_get_name (GtkSourceStyleScheme *scheme); - const gchar *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme); - - const gchar *gtk_source_style_scheme_get_filename (GtkSourceStyleScheme *scheme); ---- 61,67 ---- - const gchar *gtk_source_style_scheme_get_name (GtkSourceStyleScheme *scheme); - const gchar *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme); - -! const gchar* const * - gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme); - - const gchar *gtk_source_style_scheme_get_filename (GtkSourceStyleScheme *scheme); -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c 2010-05-30 12:24:14.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c 2015-10-27 14:55:30.583506500 +0100 -*************** -*** 515,521 **** - * of string containing the search path. - * The array is owned by the @manager and must not be modified. - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL); ---- 515,521 ---- - * of string containing the search path. - * The array is owned by the @manager and must not be modified. - */ -! const gchar* const * - gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL); -*************** -*** 554,560 **** - * of string containing the ids of the available style schemes or %NULL if no - * style scheme is available. The array is owned by the @manager and must not be modified. - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL); ---- 554,560 ---- - * of string containing the ids of the available style schemes or %NULL if no - * style scheme is available. The array is owned by the @manager and must not be modified. - */ -! const gchar* const * - gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL); -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h 2009-11-15 00:41:33.000000000 +0100 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h 2015-10-27 14:56:24.498897500 +0100 -*************** -*** 73,84 **** - void gtk_source_style_scheme_manager_prepend_search_path (GtkSourceStyleSchemeManager *manager, - const gchar *path); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager); - - void gtk_source_style_scheme_manager_force_rescan (GtkSourceStyleSchemeManager *manager); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager); - - GtkSourceStyleScheme *gtk_source_style_scheme_manager_get_scheme (GtkSourceStyleSchemeManager *manager, ---- 73,84 ---- - void gtk_source_style_scheme_manager_prepend_search_path (GtkSourceStyleSchemeManager *manager, - const gchar *path); - -! const gchar* const * - gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager); - - void gtk_source_style_scheme_manager_force_rescan (GtkSourceStyleSchemeManager *manager); - -! const gchar* const * - gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager); - - GtkSourceStyleScheme *gtk_source_style_scheme_manager_get_scheme (GtkSourceStyleSchemeManager *manager, diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch index 23c303135d..1c6a038da9 100644 --- a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch +++ b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch @@ -1,33 +1,12 @@ -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 +diff/patch file created on Wed, Feb 20, 2019 11:29:48 AM with: +difftar-folder.sh tarballs/lablgtk-3.0.beta4.tar.gz lablgtk-3.0.beta4 1 +TARFILE= tarballs/lablgtk-3.0.beta4.tar.gz +FOLDER= lablgtk-3.0.beta4 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 +TARPREFIX= lablgtk-3.0.beta4/ +ORIGFOLDER= lablgtk-3.0.beta4.orig +--- lablgtk-3.0.beta4.orig/src/glib.ml 2019-02-11 07:08:17.000000000 +0100 ++++ lablgtk-3.0.beta4/src/glib.ml 2019-02-20 11:28:28.439137100 +0100 @@ -72,6 +72,8 @@ type id external channel_of_descr : Unix.file_descr -> channel @@ -37,22 +16,18 @@ ORIGFOLDER= lablgtk-2.18.3.orig 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 +--- lablgtk-3.0.beta4.orig/src/glib.mli 2019-02-11 07:08:17.000000000 +0100 ++++ lablgtk-3.0.beta4/src/glib.mli 2019-02-20 11:28:28.423592200 +0100 +@@ -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-3.0.beta4.orig/src/ml_glib.c 2019-02-11 07:08:17.000000000 +0100 ++++ lablgtk-3.0.beta4/src/ml_glib.c 2019-02-20 11:28:28.455395900 +0100 @@ -25,6 +25,8 @@ #include <string.h> #include <locale.h> @@ -74,7 +49,7 @@ ORIGFOLDER= lablgtk-2.18.3.orig #include "wrappers.h" #include "ml_glib.h" #include "glib_tags.h" -@@ -325,14 +332,23 @@ +@@ -326,14 +333,23 @@ #ifndef _WIN32 ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref) diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c new file mode 100755 index 0000000000..e4fdcd4d7d --- /dev/null +++ b/dev/build/windows/patches_coq/pkg-config.c @@ -0,0 +1,29 @@ +// MinGW personality wrapper for pkgconf +// This is an excutable replacement for the shell scripts /bin/ARCH-pkg-config +// Compile with e.g. +// gcc pkg-config.c -DARCH=x86_64-w64-mingw32 -o pkg-config.exe +// gcc pkg-config.c -DARCH=i686-w64-mingw32 -o pkg-config.exe +// ATTENTION: Do not compile with MinGW-gcc, compile with cygwin gcc! +// +// To test it execute e.g. +// $ ./pkg-config --path zlib +// /usr/x86_64-w64-mingw32/sys-root/mingw/lib/pkgconfig/zlib.pc + +#include <unistd.h> + +#define STRINGIFY1(arg) #arg +#define STRINGIFY(arg) STRINGIFY1(arg) + +int main(int argc, char *argv[]) +{ + // +1 for extra argument, +1 for trailing NULL + char * argvnew[argc+2]; + int id=0, is=0; + + argvnew[id++] = argv[is++]; + argvnew[id++] = "--personality="STRINGIFY(ARCH); + while( is<argc ) argvnew[id++] = argv[is++]; + argvnew[id++] = 0; + + return execv("/usr/bin/pkgconf", argvnew); +} diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch index 1afa6e7f95..1afa6e7f95 100755..100644 --- a/dev/build/windows/patches_coq/quickchick.patch +++ b/dev/build/windows/patches_coq/quickchick.patch diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 74e8d3bbaa..deeec3942d 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -289,3 +289,10 @@ : "${verdi_raft_CI_REF:=master}" : "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" : "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" + +######################################################################## +# stdlib2 +######################################################################## +: "${stdlib2_CI_REF:=master}" +: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}" +: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 2ac78d3c2b..2d242d80a4 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 -( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make | iconv -t UTF-8 -c `#9767` ) diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh index c641af2abb..d2e0ee89bf 100755 --- a/dev/ci/ci-paramcoq.sh +++ b/dev/ci/ci-paramcoq.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download paramcoq -( cd "${CI_BUILD_DIR}/paramcoq" && make && make install ) +( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples) diff --git a/dev/ci/ci-stdlib2.sh b/dev/ci/ci-stdlib2.sh new file mode 100755 index 0000000000..ec1c180d7d --- /dev/null +++ b/dev/ci/ci-stdlib2.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download stdlib2 + +( cd "${CI_BUILD_DIR}/stdlib2/src" && ./bootstrap && make && make install) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 43278c37b1..e553cbed1b 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-02-17-V1" +# CACHEKEY: "bionic_coq-V2019-03-12-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -10,7 +10,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of the image, the test-suite and external projects m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \ # Dependencies of lablgtk (for CoqIDE) - libgtk2.0-dev libgtksourceview2.0-dev \ + libgtksourceview-3.0-dev \ # Dependencies of stdlib and sphinx doc texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ @@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. -RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam +RUN wget https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam # Basic OPAM setup ENV NJOBS="2" \ @@ -37,11 +37,14 @@ ENV COMPILER="4.05.0" # 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 dune.1.6.2 ounit.2.0.8 odoc.1.3.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \ CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" +ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" + +# Must add this to COQIDE_OPAM{,_EDGE} when we update the opam +# packages "lablgtk3-gtksourceview3" # base switch RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ @@ -53,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.07.1" \ - COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ + COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" \ BASE_OPAM_EDGE="dune-release.1.1.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use diff --git a/dev/ci/nix/coq.nix b/dev/ci/nix/coq.nix index ecd280e58d..b610790f61 100644 --- a/dev/ci/nix/coq.nix +++ b/dev/ci/nix/coq.nix @@ -5,5 +5,4 @@ let coq = callPackage wd { buildDoc = false; doInstallCheck = false; coq-version coq.overrideAttrs (o: { name = "coq-local-${branch}"; src = fetchGit "${wd}"; - enableParallelBuilding = true; }) diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 94e0a666e2..17070e66ee 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -1,4 +1,4 @@ -{ pkgs ? import <nixpkgs> {} +{ pkgs ? import ../../nixpkgs.nix {} , branch , wd , project ? "xyz" @@ -20,8 +20,17 @@ let mathcomp = coqPackages.mathcomp.overrideAttrs (o: { let ssreflect = coqPackages.ssreflect.overrideAttrs (o: { inherit (mathcomp) src; }); in -let coq-ext-lib = coqPackages.coq-ext-lib; in -let simple-io = coqPackages.simple-io; in + +let coq-ext-lib = coqPackages.coq-ext-lib.overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-ext-lib/coq-ext-lib/tarball/master"; + }); in + +let simple-io = + (coqPackages.simple-io.override { inherit coq-ext-lib; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/Lysxia/coq-simple-io/tarball/master"; + }); in + let bignums = coqPackages.bignums.overrideAttrs (o: if bn == "release" then {} else if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix index 46bf02ae3c..b90f1e4f88 100644 --- a/dev/ci/nix/quickchick.nix +++ b/dev/ci/nix/quickchick.nix @@ -1,5 +1,5 @@ { ocamlPackages, ssreflect, coq-ext-lib, simple-io }: { buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ]; - coqBuildInputs = [ ssreflect coq-ext-lib simple-io ]; + coqBuildInputs = [ ssreflect simple-io ]; } diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh new file mode 100644 index 0000000000..2b4c1489ad --- /dev/null +++ b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh @@ -0,0 +1,13 @@ +_OVERLAY_BRANCH=ho-matching-occ-sel + +if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + unicoq_CI_REF="PR7819-overlay" + + mtac2_CI_REF="PR7819-overlay" + mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 + + equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + equations_CI_REF="PR7819-overlay" + +fi diff --git a/dev/ci/user-overlays/08817-sprop.sh b/dev/ci/user-overlays/08817-sprop.sh new file mode 100644 index 0000000000..81e18226ed --- /dev/null +++ b/dev/ci/user-overlays/08817-sprop.sh @@ -0,0 +1,34 @@ +if [ "$CI_PULL_REQUEST" = "8817" ] || [ "$CI_BRANCH" = "sprop" ]; then + aac_tactics_CI_REF=sprop + aac_tactics_CI_GITURL=https://github.com/SkySkimmer/aac-tactics + + coq_dpdgraph_CI_REF=sprop + coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph + + coqhammer_CI_REF=sprop + coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer + + elpi_CI_REF=sprop + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=sprop + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + ltac2_CI_REF=sprop + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + unicoq_CI_REF=sprop + unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq + + mtac2_CI_REF=sprop + mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 + + paramcoq_CI_REF=sprop + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + + quickchick_CI_REF=sprop + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + + relation_algebra_CI_REF=sprop + relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra +fi diff --git a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh new file mode 100644 index 0000000000..1110157069 --- /dev/null +++ b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9389" ] || [ "$CI_BRANCH" = "set-implicits" ]; then + + equations_CI_REF=set-implicits + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + mtac2_CI_REF=set-implicits + mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 + +fi diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh new file mode 100644 index 0000000000..1af8b5430d --- /dev/null +++ b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then + + quickchick_CI_REF=context-constructor + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + + equations_CI_REF=context-constructor + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/09678-printed-by-env.sh b/dev/ci/user-overlays/09678-printed-by-env.sh new file mode 100644 index 0000000000..ccb3498764 --- /dev/null +++ b/dev/ci/user-overlays/09678-printed-by-env.sh @@ -0,0 +1,14 @@ + +if [ "$CI_PULL_REQUEST" = "9678" ] || [ "$CI_BRANCH" = "printed-by-env" ]; then + elpi_CI_REF=printed-by-env + elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi + + equations_CI_REF=printed-by-env + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + + ltac2_CI_REF=printed-by-env + ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + quickchick_CI_REF=printed-by-env + quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick +fi diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc deleted file mode 100644 index 631fb92c97..0000000000 --- a/dev/doc/README-V1-V5.asciidoc +++ /dev/null @@ -1,378 +0,0 @@ -Notes on the prehistory of Coq -============================== -:author: Thierry Coquand, Gérard Huet & Christine Paulin-Mohring -:revdate: September 2015 -:toc: -:toc-placement: preamble -:toclevels: 1 -:showtitle: - - -This document is a copy within the Coq archive of a document written -in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin -to accompany their public release of the archive of versions 1.10 to 6.2 -of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and -implemented in the Formel team, joint between the INRIA Rocquencourt -laboratory and the Ecole Normale Supérieure of Paris, from 1984 -onwards. - -Version 1 ---------- - -This software is a prototype type-checker for a higher-order logical -formalism known as the Theory of Constructions, presented in his PhD -thesis by Thierry Coquand, with influences from Girard's system F and -de Bruijn's Automath. The metamathematical analysis of the system is -the PhD work of Thierry Coquand. The software is mostly the work of -Gérard Huet. Most of the mathematical examples verified with the -software are due to Thierry Coquand. - -The programming language of the CONSTR software (as it was called at -the time) was a version of ML adapted from the Edinburgh LCF system -and running on a LISP backend. The main improvements from the original -LCF ML were that ML was compiled rather than interpreted (Gérard Huet -building on the original translator by Lockwood Morris), and that it -was enriched by recursively defined types (work of Guy -Cousineau). This ancestor of CAML was used and improved by Larry -Paulson for his implementation of Cambridge LCF. - -Software developments of this prototype occurred from late 1983 to -early 1985. - -Version 1.10 was frozen on December 22nd 1984. It is the version used -for the examples in Thierry Coquand's thesis, defended on January 31st -1985. There was a unique binding operator, used both for universal -quantification (dependent product) at the level of types and -functional abstraction (λ) at the level of terms/proofs, in the manner -of Automath. Substitution (λ-reduction) was implemented using de -Bruijn's indexes. - -Version 1.11 was frozen on February 19th, 1985. It is the version used -for the examples in the paper: Th. Coquand, G. Huet. __Constructions: A -Higher Order Proof System for Mechanizing Mathematics__ <<CH85>>. - -Christine Paulin joined the team at this point, for her DEA research -internship. In her DEA memoir (August 1985) she presents developments -for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such -that _f(m)_ is greater than _n_, for _f_ an increasing integer -function, a challenge for constructive mathematics. She also encoded -the majority voting algorithm of Boyer and Moore. - -Version 2 ---------- - -The formal system, now renamed as the _Calculus of Constructions_, was -presented with a proof of consistency and comparisons with proof -systems of Per Martin Löf, Girard, and the Automath family of N. de -Bruijn, in the paper: T. Coquand and G. Huet. __The Calculus of -Constructions__ <<CH88>>. - -An abstraction of the software design, in the form of an abstract -machine for proof checking, and a fuller sequence of mathematical -developments was presented in: Th. Coquand, G. Huet. __Concepts -Mathématiques et Informatiques Formalisés dans le Calcul des -Constructions__<<CH87>>. - -Version 2.8 was frozen on December 16th, 1985, and served for -developing the exemples in the above papers. - -This calculus was then enriched in version 2.9 with a cumulative -hierarchy of universes. Universe levels were initially explicit -natural numbers. Another improvement was the possibility of automatic -synthesis of implicit type arguments, relieving the user of tedious -redundant declarations. - -Christine Paulin wrote an article __Algorithm development in the -Calculus of Constructions__ <<P86>>. Besides _lambo_ and _majority_, -she presents quicksort and a text formatting algorithm. - -Version 2.13 of the Calculus of Constructions with universes was -frozen on June 25th, 1986. - -A synthetic presentation of type theory along constructive lines with -ML algorithms was given by Gérard Huet in his May 1986 CMU course -notes _Formal Structures for Computation and Deduction_. Its chapter -_Induction and Recursion in the Theory of Constructions_ was presented -as an invited paper at the Joint Conference on Theory and Practice of -Software Development TAPSOFT’87 at Pise in March 1987, and published -as __Induction Principles Formalized in the Calculus of -Constructions__ <<H88>>. - -Version 3 ---------- - -This version saw the beginning of proof automation, with a search -algorithm inspired from PROLOG and the applicative logic programming -programs of the course notes _Formal structures for computation and -deduction_. The search algorithm was implemented in ML by Thierry -Coquand. The proof system could thus be used in two modes: proof -verification and proof synthesis, with tactics such as `AUTO`. - -The implementation language was now called CAML, for Categorical -Abstract Machine Language. It used as backend the LLM3 virtual machine -of Le Lisp by Jérôme Chailloux. The main developers of CAML were -Michel Mauny, Ascander Suarez and Pierre Weis. - -V3.1 was started in the summer of 1986, V3.2 was frozen at the end of -November 1986. V3.4 was developed in the first half of 1987. - -Thierry Coquand held a post-doctoral position in Cambrige University -in 1986-87, where he developed a variant implementation in SML, with -which he wrote some developments on fixpoints in Scott's domains. - -Version 4 ---------- - -This version saw the beginning of program extraction from proofs, with -two varieties of the type `Prop` of propositions, indicating -constructive intent. The proof extraction algorithms were implemented -by Christine Paulin-Mohring. - -V4.1 was frozen on July 24th, 1987. It had a first identified library -of mathematical developments (directory exemples), with libraries -Logic (containing impredicative encodings of intuitionistic logic and -algebraic primitives for booleans, natural numbers and list), `Peano` -developing second-order Peano arithmetic, `Arith` defining addition, -multiplication, euclidean division and factorial. Typical developments -were the Knaster-Tarski theorem and Newman's lemma from rewriting -theory. - -V4.2 was a joint development of a team consisting of Thierry Coquand, -Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the -log of changes. It was frozen on September 1987 as the last version -implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable -development system. - -V4.3 saw the first top-level of the system. Instead of evaluating -explicit quotations, the user could develop his mathematics in a -high-level language called the mathematical vernacular (following -Automath terminology). The user could develop files in the vernacular -notation (with .v extension) which were now separate from the `ml` -sources of the implementation. Gilles Dowek joined the team to -develop the vernacular language as his DEA internship research. - -A notion of sticky constant was introduced, in order to keep names of -lemmas when local hypotheses of proofs were discharged. This gave a -notion of global mathematical environment with local sections. - -Another significant practical change was that the system, originally -developped on the VAX central computer of our lab, was transferred on -SUN personal workstations, allowing a level of distributed -development. The extraction algorithm was modified, with three -annotations `Pos`, `Null` and `Typ` decorating the sorts `Prop` and -`Type`. - -Version 4.3 was frozen at the end of November 1987, and was -distributed to an early community of users (among those were Hugo -Herbelin and Loic Colson). - -V4.4 saw the first version of (encoded) inductive types. Now natural -numbers could be defined as: - -[source, coq] -Inductive NAT : Prop = O : NAT | Succ : NAT->NAT. - -These inductive types were encoded impredicatively in the calculus, -using a subsystem _rec_ due to Christine Paulin. V4.4 was frozen on -March 6th 1988. - -Version 4.5 was the first one to support inductive types and program -extraction. Its banner was _Calcul des Constructions avec -Réalisations et Synthèse_. The vernacular language was enriched to -accommodate extraction commands. - -The verification engine design was presented as: G. Huet. _The -Constructive Engine_. Version 4.5. Invited Conference, 2nd European -Symposium on Programming, Nancy, March 88. The final paper, -describing the V4.9 implementation, appeared in: A perspective in -Theoretical Computer Science, Commemorative Volume in memory of Gift -Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. - -Version 4.5 was demonstrated in June 1988 at the YoP Institute on -Logical Foundations of Functional Programming organized by Gérard Huet -at Austin, Texas. - -Version 4.6 was started during the summer of 1988. Its main -improvement was the complete rehaul of the proof synthesis engine by -Thierry Coquand, with a tree structure of goals. - -Its source code was communicated to Randy Pollack on September 2nd -1988. It evolved progressively into LEGO, proof system for Luo's -formalism of Extended Calculus of Constructions. - -The discharge tactic was modified by Gérard Huet to allow for -inter-dependencies in discharged lemmas. Christine Paulin improved the -inductive definition scheme in order to accommodate predicates of any -arity. - -Version 4.7 was started on September 6th, 1988. - -This version starts exploiting the CAML notion of module in order to -improve the modularity of the implementation. Now the term verifier is -identified as a proper module Machine, which the structure of its -internal data structures being hidden and thus accessible only through -the legitimate operations. This machine (the constructive engine) was -the trusted core of the implementation. The proof synthesis mechanism -was a separate proof term generator. Once a complete proof term was -synthesized with the help of tactics, it was entirely re-checked by -the engine. Thus there was no need to certify the tactics, and the -system took advantage of this fact by having tactics ignore the -universe levels, universe consistency check being relegated to the -final type-checking pass. This induced a certain puzzlement in early -users who saw, after a successful proof search, their `QED` followed -by silence, followed by a failure message due to a universe -inconsistency… - -The set of examples comprise set theory experiments by Hugo Herbelin, -and notably the Schroeder-Bernstein theorem. - -Version 4.8, started on October 8th, 1988, saw a major -re-implementation of the abstract syntax type `constr`, separating -variables of the formalism and metavariables denoting incomplete terms -managed by the search mechanism. A notion of level (with three values -`TYPE`, `OBJECT` and `PROOF`) is made explicit and a type judgement -clarifies the constructions, whose implementation is now fully -explicit. Structural equality is speeded up by using pointer equality, -yielding spectacular improvements. Thierry Coquand adapts the proof -synthesis to the new representation, and simplifies pattern matching -to first-order predicate calculus matching, with important performance -gain. - -A new representation of the universe hierarchy is then defined by -Gérard Huet. Universe levels are now implemented implicitly, through -a hidden graph of abstract levels constrained with an order relation. -Checking acyclicity of the graph insures well-foundedness of the -ordering, and thus consistency. This was documented in a memo _Adding -Type:Type to the Calculus of Constructions_ which was never published. - -The development version is released as a stable 4.8 at the end of -1988. - -Version 4.9 is released on March 1st 1989, with the new ``elastic'' -universe hierarchy. - -The spring of 1989 saw the first attempt at documenting the system -usage, with a number of papers describing the formalism: - -- _Metamathematical Investigations of a Calculus of Constructions_, by - Thierry Coquand <<C90>>, -- _Inductive definitions in the Calculus of Constructions_, by - Christine Paulin-Mohrin, -- _Extracting Fω's programs from proofs in the Calculus of - Constructions_, by Christine Paulin-Mohring <<P89>>, -- _The Constructive Engine_, by Gérard Huet <<H89>>, - -as well as a number of user guides: - -- _A short user's guide for the Constructions_ Version 4.10, by Gérard Huet -- _A Vernacular Syllabus_, by Gilles Dowek. -- _The Tactics Theorem Prover, User's guide_, Version 4.10, by Thierry - Coquand. - -Stable V4.10, released on May 1st, 1989, was then a mature system, -distributed with CAML V2.6. - -In the mean time, Thierry Coquand and Christine Paulin-Mohring had -been investigating how to add native inductive types to the Calculus -of Constructions, in the manner of Per Martin-Löf's Intuitionistic -Type Theory. The impredicative encoding had already been presented in: -F. Pfenning and C. Paulin-Mohring. __Inductively defined types in the -Calculus of Constructions__ <<PP90>>. An extension of the calculus -with primitive inductive types appeared in: Th. Coquand and -C. Paulin-Mohring. __Inductively defined types__ <<CP90>>. - -This led to the Calculus of Inductive Constructions, logical formalism -implemented in Versions 5 upward of the system, and documented in: -C. Paulin-Mohring. __Inductive Definitions in the System Coq - Rules -and Properties__ <<P93>>. - -The last version of CONSTR is Version 4.11, which was last distributed -in the spring of 1990. It was demonstrated at the first workshop of -the European Basic Research Action Logical Frameworks In Sophia -Antipolis in May 1990. - -At the end of 1989, Version 5.1 was started, and renamed as the system -Coq for the Calculus of Inductive Constructions. It was then ported to -the new stand-alone implementation of ML called Caml-light. - -In 1990 many changes occurred. Thierry Coquand left for Chalmers -University in Göteborg. Christine Paulin-Mohring took a CNRS -researcher position at the LIP laboratory of École Normale Supérieure -de Lyon. Project Formel was terminated, and gave rise to two teams: -Cristal at INRIA-Roquencourt, that continued developments in -functional programming with Caml-light then Ocaml, and Coq, continuing -the type theory research, with a joint team headed by Gérard Huet at -INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory -of CNRS-ENS Lyon. - -Chetan Murthy joined the team in 1991 and became the main software -architect of Version 5. He completely rehauled the implementation for -efficiency. Versions 5.6 and 5.8 were major distributed versions, -with complete documentation and a library of users' developements. The -use of the RCS revision control system, and systematic ChangeLog -files, allow a more precise tracking of the software developments. - -Developments from Version 6 upwards are documented in the credits -section of Coq's Reference Manual. - -==== -September 2015 + -Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. -==== - -[bibliography] -.Bibliographic references - -- [[[CH85]]] Th. Coquand, G. Huet. _Constructions: A Higher Order - Proof System for Mechanizing Mathematics_. Invited paper, EUROCAL85, - April 1985, Linz, Austria. Springer Verlag LNCS 203, pp. 151-184. - -- [[[CH88]]] T. Coquand and G. Huet. _The Calculus of Constructions_. - Submitted on June 30th 1985, accepted on December 5th, 1985, - Information and Computation. Preprint as Rapport de Recherche Inria - n°530, Mai 1986. Final version in Information and Computation - 76,2/3, Feb. 88. - -- [[[CH87]]] Th. Coquand, G. Huet. _Concepts Mathématiques et - Informatiques Formalisés dans le Calcul des Constructions_. Invited - paper, European Logic Colloquium, Orsay, July 1985. Preprint as - Rapport de recherche INRIA n°463, Dec. 85. Published in Logic - Colloquium 1985, North-Holland, 1987. - -- [[[P86]]] C. Paulin. _Algorithm development in the Calculus of - Constructions_, preprint as Rapport de recherche INRIA n°497, - March 86. Final version in Proceedings Symposium on Logic in Computer - Science, Cambridge, MA, 1986 (IEEE Computer Society Press). - -- [[[H88]]] G. Huet. _Induction Principles Formalized in the Calculus - of Constructions_ in Programming of Future Generation Computers, - Ed. K. Fuchi and M. Nivat, North-Holland, 1988. - -- [[[C90]]] Th. Coquand. _Metamathematical Investigations of a - Calculus of Constructions_, by INRIA Research Report N°1088, - Sept. 1989, published in Logic and Computer Science, - ed. P.G. Odifreddi, Academic Press, 1990. - -- [[[P89]]] C. Paulin. _Extracting F ω's programs from proofs in the - calculus of constructions_. 16th Annual ACM Symposium on Principles - of Programming Languages, Austin. 1989. - -- [[[H89]]] G. Huet. _The constructive engine_. A perspective in - Theoretical Computer Science. Commemorative Volume for Gift - Siromoney. World Scientific Publishing (1989). - -- [[[PP90]]] F. Pfenning and C. Paulin-Mohring. _Inductively defined - types in the Calculus of Constructions_. Preprint technical report - CMU-CS-89-209, final version in Proceedings of Mathematical - Foundations of Programming Semantics, volume 442, Lecture Notes in - Computer Science. Springer-Verlag, 1990 - -- [[[CP90]]] Th. Coquand and C. Paulin-Mohring. _Inductively defined - types_. In P. Martin-Löf and G. Mints, editors, Proceedings of - Colog'88, volume 417, Lecture Notes in Computer Science. - Springer-Verlag, 1990. - -- [[[P93]]] C. Paulin-Mohring. _Inductive Definitions in the System - Coq - Rules and Properties_. In M. Bezem and J.-F. Groote, editors, - Proceedings of the conference Typed Lambda Calculi and Applications, - volume 664, Lecture Notes in Computer Science, 1993. diff --git a/dev/doc/SProp.md b/dev/doc/SProp.md new file mode 100644 index 0000000000..f263dbb867 --- /dev/null +++ b/dev/doc/SProp.md @@ -0,0 +1,41 @@ +# Notes on SProp + +(ml API side, see refman for user side) + +## Relevance + +All kernel binders (`Prod`/`Lambda`/`LetIn`/`Context` elements) are +now annotated with a value in `type Sorts.relevance = Relevant | +Irrelevant`. It should verify that the binder's type lives in `SProp` +iff the annotation is `Irrelevant`. + +As a plugin you can generally just use `Relevant` everywhere, the +kernel will fix it if needed when it checks the terms you produce. The +only issue is that if you generate `Relevant` when it should have been +`Irrelevant` you won't be able to use proof irrelevance on that +variable until the kernel fixes it. See refman for examples as Coq +also uses `Relevant` incorrectly in some places. + +This annotation is done by transforming the binder name `'a` into a +`'a Context.binder_annot = { binder_name : 'a; binder_relevance : +Sorts.relevance }`, eg `Prod of Name.t * types * types` becomes `Prod +of Name.t Context.binder_annot * types * types`. + +If you just carry binder names around without looking at them no +change is needed, eg if you have `match foo with Lambda (x, a, b) -> +Prod (x, a, type_of (push_rel (LocalAssum (x,a)) env) b)`. Otherwise +see `context.mli` for a few combinators on the `binder_annot` type. + +When making `Relevant` annotations you can use some convenience +functions from `Context` (eg `annotR x = make_annot x Relevant`), also +`mkArrowR` from `Constr`/`EConstr` which has the signature of the old +`mkArrow`. + +You can enable the debug warning `bad-relevance` to help find places +where you generate incorrect annotations. + +Relevance can be inferred from a well-typed term using functions in +`Retypeops` (for `Constr`) and `Retyping` (for `EConstr`). For `x` a +term, note the difference between its relevance as a term (is `x : +(_ : SProp)`) and as a type (is `x : SProp`), there are functions for +both kinds. diff --git a/dev/doc/COMPATIBILITY b/dev/doc/archive/COMPATIBILITY index a81afca32d..a81afca32d 100644 --- a/dev/doc/COMPATIBILITY +++ b/dev/doc/archive/COMPATIBILITY diff --git a/dev/doc/extensions.txt b/dev/doc/archive/extensions.txt index 075496db7c..36d63029f1 100644 --- a/dev/doc/extensions.txt +++ b/dev/doc/archive/extensions.txt @@ -16,4 +16,3 @@ Exemple de l'ajout de l'entrée "clause": faut rejouter clause dans le GLOBAL du GEXTEND - seulement après, le nom clause sera accessible dans les TACTIC EXTEND ! - diff --git a/dev/doc/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex index 337b9226df..0b0811d81b 100644 --- a/dev/doc/naming-conventions.tex +++ b/dev/doc/archive/naming-conventions.tex @@ -133,7 +133,7 @@ has name \texttt{D\_integral}, then \end{quote} will have name \texttt{D\_integral\_inf}. -As an exception, decidability statements, such as +As an exception, decidability statements, such as \begin{quote} \begin{tt} {forall x y, \{x = y\} + \{x <> y\}} @@ -284,7 +284,7 @@ If the conclusion is in the other way than listed below, add suffix \itemrule{Nilpotency of element elt wrt a ring D with additive neutral element {\zero} and multiplicative binary operator -{\op}}{Delt\_nilpotent} +{\op}}{Delt\_nilpotent} {op elt elt = zero} Remark: We leave the ring structure of D implicit; the general definition is ``exists n, iter n op elt = zero''. @@ -487,7 +487,7 @@ binary relation {\rel}}{phi\_op\_rel, phi\_op\_rel\_morphism} {forall x y:D, phi (op x y) <-> rel (phi x) (phi y)} Remark: If the operator and the relation have similar name, one uses -\texttt{phi\_op}. +\texttt{phi\_op}. Question: How to name each direction? (add \_elim for -> and \_intro for <- ?? -- as done in Bool.v ??) diff --git a/dev/doc/newsyntax.tex b/dev/doc/archive/newsyntax.tex index d1986fa0d1..71e964bcc9 100644 --- a/dev/doc/newsyntax.tex +++ b/dev/doc/archive/newsyntax.tex @@ -50,7 +50,7 @@ La réflexion de la rénovation de la syntaxe des tactiques n'est pas encore aussi poussée que pour les termes (section~\ref{constrsyntax}), mais cette section vise à énoncer les quelques principes que l'on -souhaite suivre. +souhaite suivre. \begin{itemize} \item Réutiliser les mots-clés de la syntaxe des termes (i.e. en @@ -612,7 +612,7 @@ Fixpoint plus n m : nat {struct n} := \subsection{Questions ouvertes} Voici les points sur lesquels la discussion est particulièrement -ouverte: +ouverte: \begin{itemize} \item choix d'autres symboles pour les quantificateurs \TERM{!} et \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!} diff --git a/dev/doc/notes-on-conversion.v b/dev/doc/archive/notes-on-conversion.v index a81f170c63..a78ecd181a 100644 --- a/dev/doc/notes-on-conversion.v +++ b/dev/doc/archive/notes-on-conversion.v @@ -69,5 +69,3 @@ it is not convertible. The only hope to improve this problem is to observe that S' hides (behind two indirections) a Setoid constructor. This could be the argument to solve the problem. - - diff --git a/dev/doc/old_svn_branches.txt b/dev/doc/archive/old_svn_branches.txt index ee56ee24e9..ee56ee24e9 100644 --- a/dev/doc/old_svn_branches.txt +++ b/dev/doc/archive/old_svn_branches.txt diff --git a/dev/doc/perf-analysis b/dev/doc/archive/perf-analysis index ac54fa6f73..ac54fa6f73 100644 --- a/dev/doc/perf-analysis +++ b/dev/doc/archive/perf-analysis diff --git a/dev/doc/versions-history.tex b/dev/doc/archive/versions-history.tex index 1c4913d201..25dabad497 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/archive/versions-history.tex @@ -135,7 +135,7 @@ Coq V5.8.3& released 6 December 1993 % Announce on coq-club & & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\ -Coq V5.9 alpha& 7 July 1993 & +Coq V5.9 alpha& 7 July 1993 & experimental version based on evars refinement \\ & & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\ & & version), not released\\ @@ -159,7 +159,7 @@ Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\ \begin{tabular}{l|l|l} version & date & comments \\ \hline -Coq V5.10 ``Murthy'' & 22 January 1994 & +Coq V5.10 ``Murthy'' & 22 January 1994 & introduction of the ``DOPN'' structure\\ & & \feature{eapply/prolog} tactics\\ & & private use of cvs on madiran.inria.fr\\ @@ -179,7 +179,7 @@ Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\ Coq V5.10.9& announced on 17 August 1994 & % Announced by Catherine Parent on coqdev - % Version avec une copie de THEORIES pour les inductifs mutuels + % Version avec une copie de THEORIES pour les inductifs mutuels \\ Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\ @@ -192,7 +192,7 @@ Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\ Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\ -Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW +Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\ & & MS-DOS version released on 30 October 1995\\ @@ -203,7 +203,7 @@ Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\ Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\ % Announce on coq-club by BW - % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive + % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive & & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\ @@ -434,7 +434,7 @@ evars-based experimentation \\ & & to Coq V5.7, version from October/November 1992\\ -CtCoq & released 25 October 1995 & first beta-version \\ % Announce on coq-club by Janet +CtCoq & released 25 October 1995 & first beta-version \\ % Announce on coq-club by Janet Proto with explicit substitutions & 1997 &\\ diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index a31ab1c511..b1bfac8cc9 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -126,9 +126,9 @@ script again] This will be fixed in the future. ## Dropping from coqtop: -The following sequence is recommended: +After doing `make -f Makefile.dune voboot`, the following commands should work: ``` -dune exec coqtop.byte +dune exec dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; diff --git a/dev/doc/changes.md b/dev/doc/changes.md index e7d4b605c7..416253fad1 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -12,6 +12,8 @@ ### ML API +SProp was added, see <SProp.md> + General deprecation - All functions marked [@@ocaml.deprecated] in 8.8 have been @@ -52,6 +54,15 @@ Macros: where `atts : Vernacexpr.vernac_flags` was bound in the expression and had to be manually parsed. +- `PRINTED BY` now binds `env` and `sigma`, and expects printers which take + as parameters term printers parametrized by an environment and an `evar_map`. + +Printers + +- `Ppconstr.pr_constr_expr`, `Ppconstr.lconstr_expr`, + `Ppconstr.pr_constr_pattern_expr` and `Ppconstr.pr_lconstr_pattern_expr` + now all take an environment and an `evar_map`. + Libobject - A Higher-level API for objects with fixed scope was introduced. It supports the following kinds of objects: @@ -72,6 +83,12 @@ Libobject * `Libobject.superglobal_object` * `Libobject.superglobal_object_nodischarge` +Implicit Arguments + +- `Impargs.declare_manual_implicits` is restricted to only support declaration + of implicit binders at constant declaration time. `Impargs.set_implicits` should + be used for redeclaration of implicit arguments. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix new file mode 100644 index 0000000000..4aa0f04964 --- /dev/null +++ b/dev/nixpkgs.nix @@ -0,0 +1,4 @@ +import (fetchTarball { + url = "https://github.com/NixOS/nixpkgs/archive/2923bd5d0669f1ec6ab03ddce052e9c5efb46d8f.tar.gz"; + sha256 = "16cn93rpxfql5idhigyjyhc013a3hwzyy2dl1xv7h2p78sk728vw"; +}) diff --git a/dev/shim/dune b/dev/shim/dune index 85a0d205da..39b4ef492c 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -11,6 +11,19 @@ (run chmod +x %{targets}))))) (rule + (targets coqbyte-prelude) + (deps + %{bin:coqtop.byte} + %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so} + %{project_root}/theories/Init/Prelude.vo) + (action + (with-outputs-to %{targets} + (progn + (echo "#!/usr/bin/env bash\n") + (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \"$@\"") + (run chmod +x %{targets}))))) + +(rule (targets coqide-prelude) (deps %{bin:coqqueryworker.opt} diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a3d2f33216..499bbba37e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -20,6 +20,7 @@ open Univ open Environ open Printer open Constr +open Context open Genarg open Clenv @@ -71,7 +72,7 @@ let pr_econstr t = 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 ppconstr_expr x = let sigma,env = Pfedit.get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x) let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) @@ -306,6 +307,7 @@ let constr_display csr = incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ()) and sort_display = function + | SProp -> "SProp" | Set -> "Set" | Prop -> "Prop" | Type u -> univ_display u; @@ -315,7 +317,7 @@ let constr_display csr = Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="") then (" "^i) else "")) (Instance.to_array l) "" - and name_display = function + and name_display x = match x.binder_name with | Name id -> "Name("^(Id.to_string id)^")" | Anonymous -> "Anonymous" @@ -335,13 +337,13 @@ let print_pure_constr csr = | Cast (c,_, t) -> open_hovbox 1; print_string "("; (term_display c); print_cut(); print_string "::"; (term_display t); print_string ")"; close_box() - | Prod (Name(id),t,c) -> + | Prod ({binder_name=Name(id)},t,c) -> open_hovbox 1; print_string"("; print_string (Id.to_string id); print_string ":"; box_display t; print_string ")"; print_cut(); box_display c; close_box() - | Prod (Anonymous,t,c) -> + | Prod ({binder_name=Anonymous},t,c) -> print_string"("; box_display t; print_cut(); print_string "->"; box_display c; print_string ")"; | Lambda (na,t,c) -> @@ -430,12 +432,13 @@ let print_pure_constr csr = Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u) and sort_display = function + | SProp -> print_string "SProp" | Set -> print_string "Set" | Prop -> print_string "Prop" | Type u -> open_hbox(); print_string "Type("; pp (pr_uni u); print_string ")"; close_box() - and name_display = function + and name_display x = match x.binder_name with | Name id -> print_string (Id.to_string id) | Anonymous -> print_string "_" (* Remove the top names for library and Scratch to avoid long names *) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index dc30793a6e..863d930968 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -25,6 +25,7 @@ let print_vfix_app () = print_string "vfix_app" let print_vswith () = print_string "switch" let ppsort = function + | SProp -> print_string "SProp" | Set -> print_string "Set" | Prop -> print_string "Prop" | Type u -> print_string "Type" |