diff options
Diffstat (limited to 'dev')
21 files changed, 307 insertions, 433 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index c8cfcf60c8..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.
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 43f44a80b4..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" bin_special/pkg-config - 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-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/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index ac763547b6..e553cbed1b 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-03-11-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" \ @@ -41,7 +41,10 @@ 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/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/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/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/changes.md b/dev/doc/changes.md index 491a75bb3d..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: 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/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" |