aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitattributes4
-rw-r--r--.github/CODEOWNERS2
-rw-r--r--.gitlab-ci.yml88
-rwxr-xr-xdev/build/windows/MakeCoq_MinGW.bat976
-rw-r--r--dev/ci/appveyor.bat84
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst2
-rw-r--r--interp/constrextern.ml5
-rw-r--r--interp/notation.ml23
-rw-r--r--interp/notation.mli2
-rw-r--r--lib/util.ml6
-rw-r--r--lib/util.mli4
-rw-r--r--parsing/cLexer.ml59
-rw-r--r--parsing/cLexer.mli11
-rw-r--r--parsing/tok.ml25
-rw-r--r--plugins/ltac/tacinterp.ml4
-rw-r--r--printing/proof_diffs.ml3
-rw-r--r--test-suite/bugs/closed/bug_4781.v (renamed from test-suite/bugs/opened/bug_4781.v)16
-rw-r--r--test-suite/bugs/closed/bug_7904.v13
-rw-r--r--test-suite/output/Notations4.out2
-rw-r--r--test-suite/output/Notations4.v17
-rw-r--r--test-suite/unit-tests/printing/proof_diffs_test.ml35
21 files changed, 740 insertions, 641 deletions
diff --git a/.gitattributes b/.gitattributes
index 742ef27f49..47538be4a3 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -54,5 +54,5 @@ tools/CoqMakefile.in whitespace=blank-at-eol
# CR is desired for these Windows files.
*.bat whitespace=cr-at-eol,blank-at-eol,tab-in-indent
-* eol=lf
-*.bat eol=crlf
+# never do endline conversion
+* -text
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 0f2dd89975..b0e79fb1b2 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -314,7 +314,7 @@ azure-pipelines.yml @coq/ci-maintainers
/test-suite/README.md @gares
# Secondary maintainer @SkySkimmer
-/test-suite/save-logs @SkySkimmer
+/test-suite/report.sh @SkySkimmer
/test-suite/complexity/ @herbelin
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 596b51c3eb..f131a97ba5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -174,20 +174,17 @@ after_script:
script:
- set -e
- echo 'start:coq.test'
- - make -f Makefile.ci -j "$NJOBS" ${TEST_TARGET}
+ - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
- echo 'end:coq.test'
- set +e
dependencies:
- build:base
- variables: &ci-template-vars
- TEST_TARGET: "$CI_JOB_NAME"
.ci-template-flambda: &ci-template-flambda
<<: *ci-template
dependencies:
- build:edge+flambda
variables:
- <<: *ci-template-vars
OPAM_SWITCH: "edge"
OPAM_VARIANT: "+flambda"
@@ -457,93 +454,98 @@ validate:edge+flambda:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
-ci-aac_tactics:
- <<: *ci-template
+# Libraries are by convention the projects that depend on Coq
+# but not on its ML API
-ci-bedrock2:
+library:ci-bedrock2:
<<: *ci-template
allow_failure: true
-ci-bignums:
- <<: *ci-template
-
-ci-color:
+library:ci-color:
<<: *ci-template-flambda
-ci-compcert:
+library:ci-compcert:
<<: *ci-template-flambda
-ci-coq_dpdgraph:
+library:ci-coquelicot:
<<: *ci-template
-ci-coquelicot:
+library:ci-cross-crypto:
<<: *ci-template
-ci-cross-crypto:
+library:ci-fcsl-pcm:
<<: *ci-template
-ci-elpi:
- <<: *ci-template
+library:ci-fiat-crypto:
+ <<: *ci-template-flambda
-ci-equations:
- <<: *ci-template
+library:ci-fiat-crypto-legacy:
+ <<: *ci-template-flambda
-ci-fcsl-pcm:
+library:ci-flocq:
<<: *ci-template
-ci-fiat-crypto:
+library:ci-formal-topology:
<<: *ci-template-flambda
-ci-fiat-crypto-legacy:
+library:ci-geocoq:
<<: *ci-template-flambda
-ci-fiat-parsers:
+library:ci-hott:
<<: *ci-template
-ci-flocq:
+library:ci-iris-lambda-rust:
+ <<: *ci-template-flambda
+
+library:ci-math-comp:
+ <<: *ci-template-flambda
+
+library:ci-sf:
<<: *ci-template
-ci-formal-topology:
+library:ci-unimath:
<<: *ci-template-flambda
-ci-geocoq:
+library:ci-vst:
<<: *ci-template-flambda
-ci-coqhammer:
+# Plugins are by definition the projects that depend on Coq's ML API
+
+plugin:ci-aac_tactics:
<<: *ci-template
-ci-hott:
+plugin:ci-bignums:
<<: *ci-template
-ci-iris-lambda-rust:
- <<: *ci-template-flambda
+plugin:ci-coq_dpdgraph:
+ <<: *ci-template
-ci-ltac2:
+plugin:ci-coqhammer:
<<: *ci-template
-ci-math-comp:
- <<: *ci-template-flambda
+plugin:ci-elpi:
+ <<: *ci-template
-ci-mtac2:
+plugin:ci-equations:
<<: *ci-template
-ci-paramcoq:
+plugin:ci-fiat-parsers:
<<: *ci-template
-ci-plugin_tutorial:
+plugin:ci-ltac2:
<<: *ci-template
-ci-quickchick:
- <<: *ci-template-flambda
+plugin:ci-mtac2:
+ <<: *ci-template
-ci-relation-algebra:
+plugin:ci-paramcoq:
<<: *ci-template
-ci-sf:
+plugin:ci-plugin_tutorial:
<<: *ci-template
-ci-unimath:
+plugin:ci-quickchick:
<<: *ci-template-flambda
-ci-vst:
- <<: *ci-template-flambda
+plugin:ci-relation-algebra:
+ <<: *ci-template
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index fdbb0eca2b..8489bcfc3a 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -1,488 +1,488 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== NOTES ==========
-
-REM For Cygwin setup command line options
-REM see https://cygwin.com/faq/faq.html#faq.setup.cli
-
-REM ========== DEFAULT VALUES FOR PARAMETERS ==========
-
-REM For a description of all parameters, see ReadMe.txt
-
-SET BATCHFILE=%~0
-SET BATCHDIR=%~dp0
-
-REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
-SET ARCH=x86_64
-
-REM see -mode in ReadMe.txt
-SET INSTALLMODE=absolute
-
-REM see -installer in ReadMe.txt
-SET MAKEINSTALLER=N
-
-REM see -ocaml in ReadMe.txt
-SET INSTALLOCAML=N
-
-REM see -make in ReadMe.txt
-SET INSTALLMAKE=N
-
-REM see -destcyg in ReadMe.txt
-SET DESTCYG=C:\bin\cygwin_coq
-
-REM see -destcoq in ReadMe.txt
-SET DESTCOQ=C:\bin\coq
-
-REM see -setup in ReadMe.txt
-SET SETUP=setup-x86_64.exe
-
-REM see -proxy in ReadMe.txt
-IF DEFINED HTTP_PROXY (
- SET PROXY=%HTTP_PROXY:http://=%
-) else (
- REM One can't set a variable to empty in DOS, but you can set it to a space this way.
- REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
- SET "PROXY= "
-)
-
-REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=http://mirror.easyname.at/cygwin
-
-REM see -cygcache in ReadMe.txt
-SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
-
-REM see -cyglocal in ReadMe.txt
-SET CYGWIN_FROM_CACHE=N
-
-REM see -cygquiet in ReadMe.txt
-SET CYGWIN_QUIET=Y
-
-REM see -srccache in ReadMe.txt
-SET SOURCE_LOCAL_CACHE_WFMT=%BATCHDIR%source_cache
-
-REM see -coqver in ReadMe.txt
-SET COQ_VERSION=8.5pl3
-
-REM see -gtksrc in ReadMe.txt
-SET GTK_FROM_SOURCES=N
-
-REM see -threads in ReadMe.txt
-SET MAKE_THREADS=8
-
-REM see -addon in ReadMe.txt
-SET "COQ_ADDONS= "
-
-REM ========== PARSE COMMAND LINE PARAMETERS ==========
-
-SHIFT
-
-:Parse
-
-IF "%~0" == "-arch" (
- IF "%~1" == "32" (
- SET ARCH=i686
- SET SETUP=setup-x86.exe
- ) ELSE (
- IF "%~1" == "64" (
- SET ARCH=x86_64
- SET SETUP=setup-x86_64.exe
- ) ELSE (
- ECHO "Invalid -arch, valid are 32 and 64"
- GOTO :EOF
- )
- )
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-mode" (
- IF "%~1" == "mingwincygwin" (
- SET INSTALLMODE=%~1
- ) ELSE (
- IF "%~1" == "absolute" (
- SET INSTALLMODE=%~1
- ) ELSE (
- IF "%~1" == "relocatable" (
- SET INSTALLMODE=%~1
- ) ELSE (
- ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
- GOTO :EOF
- )
- )
- )
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-installer" (
- SET MAKEINSTALLER=%~1
- CALL :CheckYN -installer %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-ocaml" (
- SET INSTALLOCAML=%~1
- CALL :CheckYN -installer %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-make" (
- SET INSTALLMAKE=%~1
- CALL :CheckYN -installer %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-destcyg" (
- SET DESTCYG=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-destcoq" (
- SET DESTCOQ=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-setup" (
- SET SETUP=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-proxy" (
- SET PROXY=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-cygrepo" (
- SET CYGWIN_REPOSITORY=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-cygcache" (
- SET CYGWIN_LOCAL_CACHE_WFMT=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-cyglocal" (
- SET CYGWIN_FROM_CACHE=%~1
- CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-cygquiet" (
- SET CYGWIN_QUIET=%~1
- CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-srccache" (
- SET SOURCE_LOCAL_CACHE_WFMT=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-coqver" (
- SET COQ_VERSION=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-gtksrc" (
- SET GTK_FROM_SOURCES=%~1
- CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-threads" (
- SET MAKE_THREADS=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-addon" (
- SET "COQ_ADDONS=%COQ_ADDONS% %~1"
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-
-IF NOT "%~0" == "" (
- ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
- ECHO !!! Illegal parameter %~0
- ECHO Usage:
- ECHO MakeCoq_MinGW
- CALL :PrintPars
- GOTO :EOF
-)
-
-IF NOT EXIST %SETUP% (
- ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
- ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option.
- GOTO :EOF
-)
-
-REM ========== ADJUST PARAMETERS ==========
-
-IF "%INSTALLMODE%" == "mingwincygwin" (
- SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
-)
-
-IF "%MAKEINSTALLER%" == "Y" (
- SET INSTALLMODE=relocatable
-)
-
-REM ========== CONFIRM PARAMETERS ==========
-
-CALL :PrintPars
-REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
-IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
- SET /p ANSWER="Is this correct? y/n "
- IF NOT "%ANSWER%"=="y" (GOTO :EOF)
-:DontAsk
-
-REM ========== DERIVED VARIABLES ==========
-
-SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
-SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
-SET TARGET_ARCH=%ARCH%-w64-mingw32
-SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
-
-REM Convert pathes to various formats
-REM WFMT = windows format (C:\..) Used in this batch file.
-REM CFMT = cygwin format (\cygdrive\c\..) Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
-REM MFMT = MinGW format (C:/...) Used for the build, because \\ requires escaping. Mingw can handle \ and /.
-
-SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
-SET RESULT_INSTALLDIR_MFMT=%RESULT_INSTALLDIR_WFMT:\=/%
-SET SOURCE_LOCAL_CACHE_MFMT=%SOURCE_LOCAL_CACHE_WFMT:\=/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_MFMT:C:/=/cygdrive/c/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:D:/=/cygdrive/d/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:E:/=/cygdrive/e/%
-
-ECHO CYGWIN INSTALL DIR (WIN) = %CYGWIN_INSTALLDIR_WFMT%
-ECHO CYGWIN INSTALL DIR (MINGW) = %CYGWIN_INSTALLDIR_MFMT%
-ECHO CYGWIN INSTALL DIR (CYGWIN) = %CYGWIN_INSTALLDIR_CFMT%
-ECHO RESULT INSTALL DIR (WIN) = %RESULT_INSTALLDIR_WFMT%
-ECHO RESULT INSTALL DIR (MINGW) = %RESULT_INSTALLDIR_MFMT%
-ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT%
-
-REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset
-SET MAKE_OPT=-j %MAKE_THREADS%
-
-REM ========== DERIVED CYGWIN SETUP OPTIONS ==========
-
-REM One can't set a variable to empty in DOS, but you can set it to a space this way.
-REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
-SET "CYGWIN_OPT= "
-
-IF "%CYGWIN_FROM_CACHE%" == "Y" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -L
-)
-
-IF "%CYGWIN_QUIET%" == "Y" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
-)
-
-IF "%GTK_FROM_SOURCES%"=="N" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
-)
-
-REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
-REM Otherwise chmod won't work and e.g. the ocaml build will fail.
-REM Cygwin setup does not touch the ACLs of existing folders.
-
-REM Run Cygwin Setup
-
-SET RUNSETUP=Y
-IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
- SET RUNSETUP=N
-)
-IF NOT "%CYGWIN_QUIET%" == "Y" (
- SET RUNSETUP=Y
-)
-
-IF "%COQREGTESTING%" == "Y" (
- ECHO "========== REMOVE EXISTING CYGWIN =========="
- DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL
- SET RUNSETUP=Y
-)
-
-SET "EXTRAPACKAGES= "
-
-IF NOT "%APPVEYOR%" == "True" (
- SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5
-)
-
-ECHO "========== INSTALL CYGWIN =========="
-
-IF "%RUNSETUP%"=="Y" (
- %SETUP% ^
- --proxy "%PROXY%" ^
- --site "%CYGWIN_REPOSITORY%" ^
- --root "%CYGWIN_INSTALLDIR_WFMT%" ^
- --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
- --no-shortcuts ^
- %CYGWIN_OPT% ^
- -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 mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
- -P libiconv-devel,libunistring-devel,libncurses-devel ^
- -P gettext-devel,libgettextpo-devel ^
- -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
- -P libfontconfig1 ^
- -P gtk-update-icon-cache ^
- -P libtool,automake ^
- -P intltool ^
- %EXTRAPACKAGES% ^
- || GOTO ErrorExit
-
- MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
- MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
-)
-
-IF NOT "%CYGWIN_QUIET%" == "Y" (
- REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
- REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
- :waitsetup
- tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
- IF ERRORLEVEL 1 GOTO waitsetup
-)
-
-ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
-
-REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear
-REM HOME (otherwise we get to the home directory of the other installation)
-REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user)
-SET "HOME="
-SET "PROFILEREAD="
-
-copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
-%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
-
-ECHO ========== BUILD COQ ==========
-
-MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
-MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
-
-COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
-COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
-
-%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
-
-ECHO ========== FINISHED ==========
-
-GOTO :EOF
-
-ECHO ========== BATCH FUNCTIONS ==========
-
-:PrintPars
- REM 01234567890123456789012345678901234567890123456789012345678901234567890123456789
- ECHO -arch ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
- ECHO -mode ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
- ECHO ^<absoloute = install coq in -destcoq absulute path^>
- ECHO ^<relocatable = install relocatable coq in -destcoq path^>
- ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
- ECHO -ocaml ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
- ECHO -make ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
- ECHO -destcyg ^<path to cygwin destination folder^>
- ECHO -destcoq ^<path to coq destination folder (mode=absoloute/relocatable)^>
- ECHO -setup ^<cygwin setup program name^> (auto adjusted to -arch)
- ECHO -proxy ^<internet proxy^>
- ECHO -cygrepo ^<cygwin download repository^>
- ECHO -cygcache ^<local cygwin repository/cache^>
- ECHO -cyglocal ^<Y or N^> install cygwin from cache
- ECHO -cygquiet ^<Y or N^> install cygwin without user interaction
- ECHO -srccache ^<local source code repository/cache^>
- ECHO -coqver ^<Coq version to install^>
- ECHO -gtksrc ^<Y or N^> build GTK ^(90 min^) or use cygwin version
- ECHO -threads ^<1..N^> Number of make threads
- ECHO -addon ^<name^> Enable building selected addon (can be repeated)
- ECHO(
- ECHO See ReadMe.txt for a detailed description of all parameters
- ECHO(
- ECHO Parameter values (default or currently set):
- ECHO -arch = %ARCH%
- ECHO -mode = %INSTALLMODE%
- ECHO -ocaml = %INSTALLOCAML%
- ECHO -installer= %MAKEINSTALLER%
- ECHO -make = %INSTALLMAKE%
- ECHO -destcyg = %DESTCYG%
- ECHO -destcoq = %DESTCOQ%
- ECHO -setup = %SETUP%
- ECHO -proxy = %PROXY%
- ECHO -cygrepo = %CYGWIN_REPOSITORY%
- ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
- ECHO -cyglocal = %CYGWIN_FROM_CACHE%
- ECHO -cygquiet = %CYGWIN_QUIET%
- ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
- ECHO -coqver = %COQ_VERSION%
- ECHO -gtksrc = %GTK_FROM_SOURCES%
- ECHO -threads = %MAKE_THREADS%
- ECHO -addon = %COQ_ADDONS%
- GOTO :EOF
-
-:CheckYN
- REM Reset errorlevel to 0
- CMD /c "EXIT /b 0"
- IF "%2" == "Y" (
- REM OK Y
- ) ELSE IF "%2" == "N" (
- REM OK N
- ) ELSE (
- ECHO ERROR Parameter %1 must be Y or N, but is %2
- GOTO ErrorExit
- )
- GOTO :EOF
-
-:ErrorExit
- ECHO ERROR MakeCoq_MinGW.bat failed
- EXIT /b 1
+@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== NOTES ==========
+
+REM For Cygwin setup command line options
+REM see https://cygwin.com/faq/faq.html#faq.setup.cli
+
+REM ========== DEFAULT VALUES FOR PARAMETERS ==========
+
+REM For a description of all parameters, see ReadMe.txt
+
+SET BATCHFILE=%~0
+SET BATCHDIR=%~dp0
+
+REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
+SET ARCH=x86_64
+
+REM see -mode in ReadMe.txt
+SET INSTALLMODE=absolute
+
+REM see -installer in ReadMe.txt
+SET MAKEINSTALLER=N
+
+REM see -ocaml in ReadMe.txt
+SET INSTALLOCAML=N
+
+REM see -make in ReadMe.txt
+SET INSTALLMAKE=N
+
+REM see -destcyg in ReadMe.txt
+SET DESTCYG=C:\bin\cygwin_coq
+
+REM see -destcoq in ReadMe.txt
+SET DESTCOQ=C:\bin\coq
+
+REM see -setup in ReadMe.txt
+SET SETUP=setup-x86_64.exe
+
+REM see -proxy in ReadMe.txt
+IF DEFINED HTTP_PROXY (
+ SET PROXY=%HTTP_PROXY:http://=%
+) else (
+ REM One can't set a variable to empty in DOS, but you can set it to a space this way.
+ REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+ SET "PROXY= "
+)
+
+REM see -cygrepo in ReadMe.txt
+SET CYGWIN_REPOSITORY=http://mirror.easyname.at/cygwin
+
+REM see -cygcache in ReadMe.txt
+SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
+
+REM see -cyglocal in ReadMe.txt
+SET CYGWIN_FROM_CACHE=N
+
+REM see -cygquiet in ReadMe.txt
+SET CYGWIN_QUIET=Y
+
+REM see -srccache in ReadMe.txt
+SET SOURCE_LOCAL_CACHE_WFMT=%BATCHDIR%source_cache
+
+REM see -coqver in ReadMe.txt
+SET COQ_VERSION=8.5pl3
+
+REM see -gtksrc in ReadMe.txt
+SET GTK_FROM_SOURCES=N
+
+REM see -threads in ReadMe.txt
+SET MAKE_THREADS=8
+
+REM see -addon in ReadMe.txt
+SET "COQ_ADDONS= "
+
+REM ========== PARSE COMMAND LINE PARAMETERS ==========
+
+SHIFT
+
+:Parse
+
+IF "%~0" == "-arch" (
+ IF "%~1" == "32" (
+ SET ARCH=i686
+ SET SETUP=setup-x86.exe
+ ) ELSE (
+ IF "%~1" == "64" (
+ SET ARCH=x86_64
+ SET SETUP=setup-x86_64.exe
+ ) ELSE (
+ ECHO "Invalid -arch, valid are 32 and 64"
+ GOTO :EOF
+ )
+ )
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-mode" (
+ IF "%~1" == "mingwincygwin" (
+ SET INSTALLMODE=%~1
+ ) ELSE (
+ IF "%~1" == "absolute" (
+ SET INSTALLMODE=%~1
+ ) ELSE (
+ IF "%~1" == "relocatable" (
+ SET INSTALLMODE=%~1
+ ) ELSE (
+ ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
+ GOTO :EOF
+ )
+ )
+ )
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-installer" (
+ SET MAKEINSTALLER=%~1
+ CALL :CheckYN -installer %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-ocaml" (
+ SET INSTALLOCAML=%~1
+ CALL :CheckYN -installer %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-make" (
+ SET INSTALLMAKE=%~1
+ CALL :CheckYN -installer %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-destcyg" (
+ SET DESTCYG=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-destcoq" (
+ SET DESTCOQ=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-setup" (
+ SET SETUP=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-proxy" (
+ SET PROXY=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-cygrepo" (
+ SET CYGWIN_REPOSITORY=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-cygcache" (
+ SET CYGWIN_LOCAL_CACHE_WFMT=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-cyglocal" (
+ SET CYGWIN_FROM_CACHE=%~1
+ CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-cygquiet" (
+ SET CYGWIN_QUIET=%~1
+ CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-srccache" (
+ SET SOURCE_LOCAL_CACHE_WFMT=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-coqver" (
+ SET COQ_VERSION=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-gtksrc" (
+ SET GTK_FROM_SOURCES=%~1
+ CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-threads" (
+ SET MAKE_THREADS=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-addon" (
+ SET "COQ_ADDONS=%COQ_ADDONS% %~1"
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+
+IF NOT "%~0" == "" (
+ ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
+ ECHO !!! Illegal parameter %~0
+ ECHO Usage:
+ ECHO MakeCoq_MinGW
+ CALL :PrintPars
+ GOTO :EOF
+)
+
+IF NOT EXIST %SETUP% (
+ ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
+ ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option.
+ GOTO :EOF
+)
+
+REM ========== ADJUST PARAMETERS ==========
+
+IF "%INSTALLMODE%" == "mingwincygwin" (
+ SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
+)
+
+IF "%MAKEINSTALLER%" == "Y" (
+ SET INSTALLMODE=relocatable
+)
+
+REM ========== CONFIRM PARAMETERS ==========
+
+CALL :PrintPars
+REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
+IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
+ SET /p ANSWER="Is this correct? y/n "
+ IF NOT "%ANSWER%"=="y" (GOTO :EOF)
+:DontAsk
+
+REM ========== DERIVED VARIABLES ==========
+
+SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
+SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
+SET TARGET_ARCH=%ARCH%-w64-mingw32
+SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
+
+REM Convert pathes to various formats
+REM WFMT = windows format (C:\..) Used in this batch file.
+REM CFMT = cygwin format (\cygdrive\c\..) Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
+REM MFMT = MinGW format (C:/...) Used for the build, because \\ requires escaping. Mingw can handle \ and /.
+
+SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
+SET RESULT_INSTALLDIR_MFMT=%RESULT_INSTALLDIR_WFMT:\=/%
+SET SOURCE_LOCAL_CACHE_MFMT=%SOURCE_LOCAL_CACHE_WFMT:\=/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_MFMT:C:/=/cygdrive/c/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:D:/=/cygdrive/d/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:E:/=/cygdrive/e/%
+
+ECHO CYGWIN INSTALL DIR (WIN) = %CYGWIN_INSTALLDIR_WFMT%
+ECHO CYGWIN INSTALL DIR (MINGW) = %CYGWIN_INSTALLDIR_MFMT%
+ECHO CYGWIN INSTALL DIR (CYGWIN) = %CYGWIN_INSTALLDIR_CFMT%
+ECHO RESULT INSTALL DIR (WIN) = %RESULT_INSTALLDIR_WFMT%
+ECHO RESULT INSTALL DIR (MINGW) = %RESULT_INSTALLDIR_MFMT%
+ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT%
+
+REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset
+SET MAKE_OPT=-j %MAKE_THREADS%
+
+REM ========== DERIVED CYGWIN SETUP OPTIONS ==========
+
+REM One can't set a variable to empty in DOS, but you can set it to a space this way.
+REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+SET "CYGWIN_OPT= "
+
+IF "%CYGWIN_FROM_CACHE%" == "Y" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -L
+)
+
+IF "%CYGWIN_QUIET%" == "Y" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
+)
+
+IF "%GTK_FROM_SOURCES%"=="N" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+)
+
+REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
+REM Otherwise chmod won't work and e.g. the ocaml build will fail.
+REM Cygwin setup does not touch the ACLs of existing folders.
+
+REM Run Cygwin Setup
+
+SET RUNSETUP=Y
+IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
+ SET RUNSETUP=N
+)
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+ SET RUNSETUP=Y
+)
+
+IF "%COQREGTESTING%" == "Y" (
+ ECHO "========== REMOVE EXISTING CYGWIN =========="
+ DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL
+ SET RUNSETUP=Y
+)
+
+SET "EXTRAPACKAGES= "
+
+IF NOT "%APPVEYOR%" == "True" (
+ SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5
+)
+
+ECHO "========== INSTALL CYGWIN =========="
+
+IF "%RUNSETUP%"=="Y" (
+ %SETUP% ^
+ --proxy "%PROXY%" ^
+ --site "%CYGWIN_REPOSITORY%" ^
+ --root "%CYGWIN_INSTALLDIR_WFMT%" ^
+ --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
+ --no-shortcuts ^
+ %CYGWIN_OPT% ^
+ -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 mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+ -P libiconv-devel,libunistring-devel,libncurses-devel ^
+ -P gettext-devel,libgettextpo-devel ^
+ -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
+ -P libfontconfig1 ^
+ -P gtk-update-icon-cache ^
+ -P libtool,automake ^
+ -P intltool ^
+ %EXTRAPACKAGES% ^
+ || GOTO ErrorExit
+
+ MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+ MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
+)
+
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+ REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
+ REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
+ :waitsetup
+ tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
+ IF ERRORLEVEL 1 GOTO waitsetup
+)
+
+ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
+
+REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear
+REM HOME (otherwise we get to the home directory of the other installation)
+REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user)
+SET "HOME="
+SET "PROFILEREAD="
+
+copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
+
+ECHO ========== BUILD COQ ==========
+
+MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
+
+COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
+COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
+
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
+
+ECHO ========== FINISHED ==========
+
+GOTO :EOF
+
+ECHO ========== BATCH FUNCTIONS ==========
+
+:PrintPars
+ REM 01234567890123456789012345678901234567890123456789012345678901234567890123456789
+ ECHO -arch ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
+ ECHO -mode ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
+ ECHO ^<absoloute = install coq in -destcoq absulute path^>
+ ECHO ^<relocatable = install relocatable coq in -destcoq path^>
+ ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
+ ECHO -ocaml ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
+ ECHO -make ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
+ ECHO -destcyg ^<path to cygwin destination folder^>
+ ECHO -destcoq ^<path to coq destination folder (mode=absoloute/relocatable)^>
+ ECHO -setup ^<cygwin setup program name^> (auto adjusted to -arch)
+ ECHO -proxy ^<internet proxy^>
+ ECHO -cygrepo ^<cygwin download repository^>
+ ECHO -cygcache ^<local cygwin repository/cache^>
+ ECHO -cyglocal ^<Y or N^> install cygwin from cache
+ ECHO -cygquiet ^<Y or N^> install cygwin without user interaction
+ ECHO -srccache ^<local source code repository/cache^>
+ ECHO -coqver ^<Coq version to install^>
+ ECHO -gtksrc ^<Y or N^> build GTK ^(90 min^) or use cygwin version
+ ECHO -threads ^<1..N^> Number of make threads
+ ECHO -addon ^<name^> Enable building selected addon (can be repeated)
+ ECHO(
+ ECHO See ReadMe.txt for a detailed description of all parameters
+ ECHO(
+ ECHO Parameter values (default or currently set):
+ ECHO -arch = %ARCH%
+ ECHO -mode = %INSTALLMODE%
+ ECHO -ocaml = %INSTALLOCAML%
+ ECHO -installer= %MAKEINSTALLER%
+ ECHO -make = %INSTALLMAKE%
+ ECHO -destcyg = %DESTCYG%
+ ECHO -destcoq = %DESTCOQ%
+ ECHO -setup = %SETUP%
+ ECHO -proxy = %PROXY%
+ ECHO -cygrepo = %CYGWIN_REPOSITORY%
+ ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
+ ECHO -cyglocal = %CYGWIN_FROM_CACHE%
+ ECHO -cygquiet = %CYGWIN_QUIET%
+ ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
+ ECHO -coqver = %COQ_VERSION%
+ ECHO -gtksrc = %GTK_FROM_SOURCES%
+ ECHO -threads = %MAKE_THREADS%
+ ECHO -addon = %COQ_ADDONS%
+ GOTO :EOF
+
+:CheckYN
+ REM Reset errorlevel to 0
+ CMD /c "EXIT /b 0"
+ IF "%2" == "Y" (
+ REM OK Y
+ ) ELSE IF "%2" == "N" (
+ REM OK N
+ ) ELSE (
+ ECHO ERROR Parameter %1 must be Y or N, but is %2
+ GOTO ErrorExit
+ )
+ GOTO :EOF
+
+:ErrorExit
+ ECHO ERROR MakeCoq_MinGW.bat failed
+ EXIT /b 1
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index 85a71baf7f..341b875edc 100644
--- a/dev/ci/appveyor.bat
+++ b/dev/ci/appveyor.bat
@@ -1,42 +1,42 @@
-REM This script either runs the test suite with OPAM (if USEOPAM is true) or
-REM builds the Coq binary packages for windows (if USEOPAM is false).
-
-if %ARCH% == 32 (
- SET ARCHLONG=i686
- SET CYGROOT=C:\cygwin
- SET SETUP=setup-x86.exe
-)
-
-if %ARCH% == 64 (
- SET ARCHLONG=x86_64
- SET CYGROOT=C:\cygwin64
- SET SETUP=setup-x86_64.exe
-)
-
-SET CYGCACHE=%CYGROOT%\var\cache\setup
-SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/%
-SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/%
-SET DESTCOQ=C:\coq%ARCH%_inst
-SET COQREGTESTING=Y
-
-if %USEOPAM% == false (
- call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
- -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
- -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
- -addon=bignums -make=N ^
- -setup %CYGROOT%\%SETUP% || GOTO ErrorExit
- copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
- 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
-)
-
-if %USEOPAM% == true (
- %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
- -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
- %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit
-)
-
-GOTO :EOF
-
-:ErrorExit
- ECHO ERROR %0 failed
- EXIT /b 1
+REM This script either runs the test suite with OPAM (if USEOPAM is true) or
+REM builds the Coq binary packages for windows (if USEOPAM is false).
+
+if %ARCH% == 32 (
+ SET ARCHLONG=i686
+ SET CYGROOT=C:\cygwin
+ SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+ SET ARCHLONG=x86_64
+ SET CYGROOT=C:\cygwin64
+ SET SETUP=setup-x86_64.exe
+)
+
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/%
+SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/%
+SET DESTCOQ=C:\coq%ARCH%_inst
+SET COQREGTESTING=Y
+
+if %USEOPAM% == false (
+ call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+ -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
+ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+ -addon=bignums -make=N ^
+ -setup %CYGROOT%\%SETUP% || GOTO ErrorExit
+ copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
+ 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+)
+
+if %USEOPAM% == true (
+ %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
+ -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
+ %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit
+)
+
+GOTO :EOF
+
+:ErrorExit
+ ECHO ERROR %0 failed
+ EXIT /b 1
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 1a33a9a46e..8fa631174f 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -230,7 +230,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`.
themselves are typing the proofs. We denote propositions by :production:`form`.
This constitutes a semantic subclass of the syntactic class :token:`term`.
-- :g:`Set` is is the universe of *program types* or *specifications*. The
+- :g:`Set` is the universe of *program types* or *specifications*. The
specifications themselves are typing the programs. We denote
specifications by :production:`specif`. This constitutes a semantic subclass of
the syntactic class :token:`term`.
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0d0b6158d9..444ac5ab6d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -67,10 +67,7 @@ let print_no_symbol = ref false
(**********************************************************************)
(* Turning notations and scopes on and off for printing *)
-module IRuleSet = Set.Make(struct
- type t = interp_rule
- let compare x y = Pervasives.compare x y
- end)
+module IRuleSet = InterpRuleSet
let inactive_notations_table =
Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty)
diff --git a/interp/notation.ml b/interp/notation.ml
index b0854de4a3..ca27d439fb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -50,15 +50,25 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with
| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
| (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
+let notation_entry_level_compare s1 s2 = match (s1,s2) with
+| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> 0
+| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) ->
+ pair_compare String.compare Int.compare (s1,n1) (s2,n2)
+| InConstrEntrySomeLevel, _ -> -1
+| InCustomEntryLevel _, _ -> 1
+
let notation_eq (from1,ntn1) (from2,ntn2) =
notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
+let notation_compare =
+ pair_compare notation_entry_level_compare String.compare
+
module NotationOrd =
struct
type t = notation
- let compare = Pervasives.compare
+ let compare = notation_compare
end
module NotationSet = Set.Make(NotationOrd)
@@ -178,6 +188,17 @@ type scoped_notation_rule_core = scope_name * notation * interpretation * int op
type notation_rule_core = interp_rule * interpretation * int option
type notation_rule = notation_rule_core * delimiters option * bool
+let interp_rule_compare r1 r2 = match r1, r2 with
+ | NotationRule (sc1,ntn1), NotationRule (sc2,ntn2) ->
+ pair_compare (Option.compare String.compare) notation_compare (sc1,ntn1) (sc2,ntn2)
+ | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2
+ | (NotationRule _ | SynDefRule _), _ -> -1
+
+module InterpRuleSet = Set.Make(struct
+ type t = interp_rule
+ let compare = interp_rule_compare
+ end)
+
(* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and *)
type uninterp_scope_elem =
diff --git a/interp/notation.mli b/interp/notation.mli
index 75034cad70..a482e00e81 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -210,6 +210,8 @@ type interp_rule =
| NotationRule of scope_name option * notation
| SynDefRule of KerName.t
+module InterpRuleSet : Set.S with type elt = interp_rule
+
val declare_notation_interpretation : notation -> scope_name option ->
interpretation -> notation_location -> onlyprint:bool -> unit
diff --git a/lib/util.ml b/lib/util.ml
index 38d73d3453..0389336258 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -20,6 +20,12 @@ let on_pi1 f (a,b,c) = (f a,b,c)
let on_pi2 f (a,b,c) = (a,f b,c)
let on_pi3 f (a,b,c) = (a,b,f c)
+(* Comparing pairs *)
+
+let pair_compare cmpx cmpy (x1,y1 as p1) (x2,y2 as p2) =
+ if p1 == p2 then 0 else
+ let c = cmpx x1 x2 in if c == 0 then cmpy y1 y2 else c
+
(* Projections from triplets *)
let pi1 (a,_,_) = a
diff --git a/lib/util.mli b/lib/util.mli
index 1eb60f509a..fa3b622621 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -17,6 +17,10 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b
+(** Comparing pairs *)
+
+val pair_compare : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b -> 'a * 'b -> int)
+
(** Mapping under triple *)
val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index c2b7fa117d..49d6cf01d9 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -548,20 +548,27 @@ let process_sequence loc bp c cs =
aux 1 cs
(* Must be a special token *)
-let process_chars loc bp c cs =
+let process_chars ~diff_mode loc bp c cs =
let t = progress_from_byte loc None (-1) !token_tree cs c in
let ep = Stream.count cs in
match t with
| Some t -> (KEYWORD t, set_loc_pos loc bp ep)
| None ->
let ep' = bp + utf8_char_size loc cs c in
- njunk (ep' - ep) cs;
- let loc = set_loc_pos loc bp ep' in
- err loc Undefined_token
+ if diff_mode then begin
+ let len = ep' - bp in
+ ignore (store 0 c);
+ ignore (nstore (len - 1) 1 cs);
+ IDENT (get_buff len), set_loc_pos loc bp ep
+ end else begin
+ njunk (ep' - ep) cs;
+ let loc = set_loc_pos loc bp ep' in
+ err loc Undefined_token
+ end
(* Parse what follows a dot *)
-let parse_after_dot loc c bp s = match Stream.peek s with
+let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with
| Some ('a'..'z' | 'A'..'Z' | '_' as d) ->
Stream.junk s;
let len =
@@ -576,11 +583,11 @@ let parse_after_dot loc c bp s = match Stream.peek s with
let len = ident_tail loc (nstore n 0 s) s in
let field = get_buff len in
(try find_keyword loc ("."^field) s with Not_found -> FIELD field)
- | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s)
+ | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars ~diff_mode loc bp c s)
(* Parse what follows a question mark *)
-let parse_after_qmark loc bp s =
+let parse_after_qmark ~diff_mode loc bp s =
match Stream.peek s with
| Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK
| None -> KEYWORD "?"
@@ -588,7 +595,7 @@ let parse_after_qmark loc bp s =
match lookup_utf8 loc s with
| Utf8Token (st, _) when Unicode.is_valid_ident_initial st -> LEFTQMARK
| AsciiChar | Utf8Token _ | EmptyStream ->
- fst (process_chars loc bp '?' s)
+ fst (process_chars ~diff_mode loc bp '?' s)
let blank_or_eof cs =
match Stream.peek cs with
@@ -598,20 +605,20 @@ let blank_or_eof cs =
(* Parse a token in a char stream *)
-let rec next_token loc s =
+let rec next_token ~diff_mode loc s =
let bp = Stream.count s in
match Stream.peek s with
| Some ('\n' as c) ->
Stream.junk s;
let ep = Stream.count s in
- comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s
+ comm_loc bp; push_char c; next_token ~diff_mode (bump_loc_line loc ep) s
| Some (' ' | '\t' | '\r' as c) ->
Stream.junk s;
- comm_loc bp; push_char c; next_token loc s
+ comm_loc bp; push_char c; next_token ~diff_mode loc s
| Some ('.' as c) ->
Stream.junk s;
let t =
- try parse_after_dot loc c bp s with
+ try parse_after_dot ~diff_mode loc c bp s with
Stream.Failure -> raise (Stream.Error "")
in
let ep = Stream.count s in
@@ -630,13 +637,13 @@ let rec next_token loc s =
Stream.junk s;
let t,new_between_commands =
if !between_commands then process_sequence loc bp c s, true
- else process_chars loc bp c s,false
+ else process_chars ~diff_mode loc bp c s,false
in
comment_stop bp; between_commands := new_between_commands; t
| Some '?' ->
Stream.junk s;
let ep = Stream.count s in
- let t = parse_after_qmark loc bp s in
+ let t = parse_after_qmark ~diff_mode loc bp s in
comment_stop bp; (t, set_loc_pos loc bp ep)
| Some ('a'..'z' | 'A'..'Z' | '_' as c) ->
Stream.junk s;
@@ -670,12 +677,16 @@ let rec next_token loc s =
Stream.junk s;
begin try
match Stream.peek s with
+ | Some '*' when diff_mode ->
+ Stream.junk s;
+ let ep = Stream.count s in
+ (IDENT "(*", set_loc_pos loc bp ep)
| Some '*' ->
Stream.junk s;
comm_loc bp;
push_string "(*";
- let loc = comment loc bp s in next_token loc s
- | _ -> let t = process_chars loc bp c s in comment_stop bp; t
+ let loc = comment loc bp s in next_token ~diff_mode loc s
+ | _ -> let t = process_chars ~diff_mode loc bp c s in comment_stop bp; t
with Stream.Failure -> raise (Stream.Error "")
end
| Some ('{' | '}' as c) ->
@@ -683,7 +694,7 @@ let rec next_token loc s =
let ep = Stream.count s in
let t,new_between_commands =
if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true
- else process_chars loc bp c s, false
+ else process_chars ~diff_mode loc bp c s, false
in
comment_stop bp; between_commands := new_between_commands; t
| _ ->
@@ -695,14 +706,14 @@ let rec next_token loc s =
comment_stop bp;
(try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
| AsciiChar | Utf8Token _ ->
- let t = process_chars loc bp (Stream.next s) s in
+ let t = process_chars ~diff_mode loc bp (Stream.next s) s in
comment_stop bp; t
| EmptyStream ->
comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
(* (* Debug: uncomment this for tracing tokens seen by coq...*)
-let next_token loc s =
- let (t,loc as r) = next_token loc s in
+let next_token ~diff_mode loc s =
+ let (t,loc as r) = next_token ~diff_mode loc s in
Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t);
r *)
@@ -743,7 +754,7 @@ let token_text = function
| (con, "") -> con
| (con, prm) -> con ^ " \"" ^ prm ^ "\""
-let func cs =
+let func next_token cs =
let loct = loct_create () in
let cur_loc = ref (Loc.create !current_file 1 0 0 0) in
let ts =
@@ -755,8 +766,8 @@ let func cs =
in
(ts, loct_func loct)
-let lexer = {
- Plexing.tok_func = func;
+let make_lexer ~diff_mode = {
+ Plexing.tok_func = func (next_token ~diff_mode);
Plexing.tok_using =
(fun pat -> match Tok.of_pattern pat with
| KEYWORD s -> add_keyword s
@@ -765,6 +776,8 @@ let lexer = {
Plexing.tok_match = Tok.match_pattern;
Plexing.tok_text = token_text }
+let lexer = make_lexer ~diff_mode:false
+
(** Terminal symbols interpretation *)
let is_ident_not_keyword s =
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index c0ebdd45ef..af3fd7f318 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -56,3 +56,14 @@ val set_lexer_state : lexer_state -> unit
val get_lexer_state : unit -> lexer_state
val drop_lexer_state : unit -> unit
val get_comment_state : lexer_state -> ((int * int) * string) list
+
+(** Create a lexer. true enables alternate handling for computing diffs.
+It ensures that, ignoring white space, the concatenated tokens equal the input
+string. Specifically:
+- for strings, return the enclosing quotes as tokens and treat the quoted value
+as if it was unquoted, possibly becoming multiple tokens
+- for comments, return the "(*" as a token and treat the contents of the comment as if
+it was not in a comment, possibly becoming multiple tokens
+- return any unrecognized Ascii or UTF-8 character as a string
+*)
+val make_lexer : diff_mode:bool -> Tok.t Gramlib.Plexing.lexer
diff --git a/parsing/tok.ml b/parsing/tok.ml
index c0d5b6742d..03825e350f 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -40,18 +40,19 @@ let extract_string diff_mode = function
| KEYWORD s -> s
| IDENT s -> s
| STRING s ->
- if diff_mode then
- let escape_quotes s =
- let len = String.length s in
- let buf = Buffer.create len in
- for i = 0 to len-1 do
- let ch = String.get s i in
- Buffer.add_char buf ch;
- if ch = '"' then Buffer.add_char buf '"' else ()
- done;
- Buffer.contents buf
- in
- "\"" ^ (escape_quotes s) ^ "\"" else s
+ if diff_mode then
+ let escape_quotes s =
+ let len = String.length s in
+ let buf = Buffer.create len in
+ for i = 0 to len-1 do
+ let ch = String.get s i in
+ Buffer.add_char buf ch;
+ if ch = '"' then Buffer.add_char buf '"' else ()
+ done;
+ Buffer.contents buf
+ in
+ "\"" ^ (escape_quotes s) ^ "\""
+ else s
| PATTERNIDENT s -> s
| FIELD s -> if diff_mode then "." ^ s else s
| INT s -> s
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ae4cd06022..3e7479903a 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1957,7 +1957,9 @@ let lifts f = (); fun ist x -> Ftactic.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let (sigma, v) = f ist env sigma x in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Ftactic.return v)
+ (* FIXME once we don't need to catch side effects *)
+ (Proofview.tclTHEN (Proofview.Unsafe.tclSETENV (Global.env()))
+ (Ftactic.return v))
end
let interp_bindings' ist bl = Ftactic.return begin fun env sigma ->
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index b280ce909b..c1ea067567 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -88,7 +88,8 @@ let tokenize_string s =
let st = CLexer.get_lexer_state () in
try
let istr = Stream.of_string s in
- let lex = CLexer.lexer.Gramlib.Plexing.tok_func istr in
+ let lexer = CLexer.make_lexer ~diff_mode:true in
+ let lex = lexer.Gramlib.Plexing.tok_func istr in
let toks = stream_tok [] (fst lex) in
CLexer.set_lexer_state st;
toks
diff --git a/test-suite/bugs/opened/bug_4781.v b/test-suite/bugs/closed/bug_4781.v
index 8b651ac22e..464a3de1b3 100644
--- a/test-suite/bugs/opened/bug_4781.v
+++ b/test-suite/bugs/closed/bug_4781.v
@@ -25,29 +25,29 @@ Goal True.
let x := match constr:(Set) with ?y => constr:(y) end in
pose x.
(* This fails with an error: *)
- Fail let term := constr:(I) in
+ let term := constr:(I) in
let T := type of term in
let x := constr:((_ : abstract_term term) : T) in
let x := match constr:(x) with ?y => constr:(y) end in
pose x. (* The command has indeed failed with message:
Error: Variable y should be bound to a term. *)
(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
- Fail let term := constr:(I) in
+ let term := constr:(I) in
let T := type of term in
let x := constr:((_ : abstract_term term) : T) in
let x := match constr:(x) with ?y => y end in
pose x.
- Fail let term := constr:(I) in
+ let term := constr:(I) in
let T := type of term in
let x := constr:((_ : abstract_term term) : T) in
let x := (eval cbv iota in x) in
pose x.
- Fail let term := constr:(I) in
+ let term := constr:(I) in
let T := type of term in
let x := constr:((_ : abstract_term term) : T) in
let x := type of x in
pose x. (* should succeed *)
- Fail let term := constr:(I) in
+ let term := constr:(I) in
let T := type of term in
let x := constr:(_ : abstract_term term) in
let x := type of x in
@@ -70,7 +70,7 @@ Even stranger, consider:*)
(*This works fine. But if I change the period to a semicolon, I get:*)
- Fail let term := constr:(I) in
+ let term := constr:(I) in
let T := type of term in
let x := constr:((_ : abstract_term term) : T) in
let y := (eval cbv iota in (let v : T := x in v)) in
@@ -82,7 +82,7 @@ Even stranger, consider:*)
(* should succeed *)
(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)
- Fail let term := constr:(I) in
+ let term := constr:(I) in
let T := type of term in
let x := constr:((_ : abstract_term term) : T) in
let y := (eval cbv iota in (let v : T := x in v)) in
@@ -92,3 +92,5 @@ Even stranger, consider:*)
let x := (eval cbv delta [x'] in x') in
let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
idtac. (* should succeed *)
+ exact I.
+Qed.
diff --git a/test-suite/bugs/closed/bug_7904.v b/test-suite/bugs/closed/bug_7904.v
new file mode 100644
index 0000000000..1e518e2adf
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7904.v
@@ -0,0 +1,13 @@
+
+
+Class abstract_term {T} (x : T) := by_abstract_term : T.
+Hint Extern 0 (@abstract_term ?T ?x) => change T; abstract (exact x) : typeclass_instances.
+
+Goal True.
+ let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let x := match constr:(x) with ?y => y end in
+ pose x as v. (* was Error: Variable x should be bound to a term but is bound to a constr. *)
+ exact v.
+Qed.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index d58e4bf2d6..94016e170b 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -45,3 +45,5 @@ fun x : nat => (x.-1)%pred
: Prop
##
: Prop
+Notation Cn := Foo.FooCn
+Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 61206b6dd0..309115848f 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -164,3 +164,20 @@ Open Scope my_scope.
Check ##.
End H.
+
+(* Fixing a bug reported by G. Gonthier in #9207 *)
+
+Module J.
+
+Module Import Mfoo.
+Module Foo.
+Definition FooCn := 2.
+Module Bar.
+Notation Cn := FooCn.
+End Bar.
+End Foo.
+Export Foo.Bar.
+End Mfoo.
+About Cn.
+
+End J.
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
index 7f9e6cc6e0..d0b8d21b69 100644
--- a/test-suite/unit-tests/printing/proof_diffs_test.ml
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -51,23 +51,28 @@ let t () =
assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed
let _ = add_test "diff_str add/remove" t
-(* example of a limitation, not really a test *)
-let t () =
- try
- let _ = diff_str "a" "&gt;" in
- assert_failure "unlexable string gives an exception"
- with _ -> ()
-let _ = add_test "diff_str unlexable" t
-
-(* problematic examples for tokenize_string:
- comments omitted
- quoted string loses quote marks (are escapes supported/handled?)
- char constant split into 2
+(* lexer tweaks:
+ comments are lexed as multiple tokens
+ strings tokens include begin/end quotes and embedded ""
+ single multibyte characters returned even if they're not keywords
+
+ inputs that give a lexer failure (but no use case needs them yet):
+ ".12"
+ unterminated string
+ invalid UTF-8 sequences
*)
let t () =
- List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx");
- cprintf "\n"
-let _ = add_test "tokenize_string examples" t
+ let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж &gt; ∃ 'c' xx" in
+ let toks = tokenize_string str in
+ (*List.iter (fun x -> cprintf "'%s' " x) toks;*)
+ (*cprintf "\n";*)
+ let str_no_white = String.concat "" (String.split_on_char ' ' str) in
+ assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks);
+ List.iter (fun s ->
+ assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks))
+ [ "(*"; "()"; ":="]
+
+let _ = add_test "tokenize_string/diff_mode in lexer" t
open Pp
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 04:26:46 +0000