diff options
98 files changed, 1288 insertions, 1119 deletions
diff --git a/.gitattributes b/.gitattributes index a5edcdb5bf..742ef27f49 100644 --- a/.gitattributes +++ b/.gitattributes @@ -53,3 +53,6 @@ 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 diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 98fe2546b5..0f2dd89975 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -37,6 +37,9 @@ *.nix @coq/nix-maintainers +azure-pipelines.yml @coq/ci-maintainers +/dev/ci/azure* @coq/ci-maintainers + ########## Documentation ########## /README.md @Zimmi48 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index de0de4cf83..108ecb5a04 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-12-05-V1" + CACHEKEY: "bionic_coq-V2018-12-14-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -367,6 +367,57 @@ test-suite:egde:dune:dev: paths: - _build/default/test-suite/logs +test-suite:edge+trunk+make: + stage: test + dependencies: [] + script: + - opam switch create 4.08.0 --empty + - eval $(opam env) + - opam repo add ocaml-pr https://github.com/ocaml/ocaml-pr-repository.git + - opam update + - opam install ocaml-variants=4.08.0 num + - eval $(opam env) + # We avoid problems with warnings: + - ./configure -profile devel -warn-error no + - make -j "$NJOBS" world + - make -j "$NJOBS" test-suite UNIT_TESTS= + variables: + OPAM_SWITCH: edge + artifacts: + name: "$CI_JOB_NAME.logs" + when: always + paths: + - test-suite/logs + expire_in: 1 week + allow_failure: true + +test-suite:edge+trunk+dune: + stage: test + dependencies: [] + script: + - opam switch create 4.08.0 --empty + - eval $(opam env) + - opam repo add ocaml-pr https://github.com/ocaml/ocaml-pr-repository.git + - opam update + - opam install ocaml-variants=4.08.0 num + - opam pin add dune --dev # ounit lablgtk conf-gtksourceview + - opam install dune + - eval $(opam env) + # We use the release profile to avoid problems with warnings + - make -f Makefile.dune trunk + - export COQ_UNIT_TEST=noop + - dune runtest --profile=ocaml408 + variables: + OPAM_SWITCH: edge + artifacts: + name: "$CI_JOB_NAME.logs" + when: always + paths: + - _build/log + - _build/default/test-suite/logs + expire_in: 1 week + allow_failure: true + validate:base: <<: *validate-template dependencies: diff --git a/Makefile.ci b/Makefile.ci index 956e3ee58f..2df6a792b6 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -60,6 +60,7 @@ ci-math-classes: ci-bignums ci-corn: ci-math-classes +ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io ci-formal-topology: ci-corn diff --git a/Makefile.dune b/Makefile.dune index 4baf3402f1..22e3271260 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -4,7 +4,7 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: quickbyte quickopt # Partial / quick developer targets .PHONY: test-suite refman-html apidoc release # Accesory targets -.PHONY: ocheck ireport clean # Maintenance targets +.PHONY: ocheck trunk ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -28,6 +28,7 @@ help: @echo " - release: build Coq in release mode" @echo "" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" + @echo " - trunk: build with a configuration compatible with OCaml trunk" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" @@ -75,6 +76,11 @@ release: voboot ocheck: voboot dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all +trunk: + dune build $(DUNEOPT) --profile=ocaml408 @vodeps + dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d + dune build $(DUNEOPT) --profile=ocaml408 coq.install coqide-server.install + ireport: dune clean dune build $(DUNEOPT) @vodeps --profile=ireport diff --git a/azure-pipelines.yml b/azure-pipelines.yml new file mode 100644 index 0000000000..e217601ae2 --- /dev/null +++ b/azure-pipelines.yml @@ -0,0 +1,31 @@ + +pool: + vmImage: 'vs2017-win2016' + +steps: +- checkout: self + fetchDepth: 10 + +# cygwin package list not checked for minimality +- script: | + powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" + SET CYGROOT=C:\cygwin64 + SET CYGCACHE=%CYGROOT%\var\cache\setup + setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python + + SET TARGET_ARCH=x86_64-w64-mingw32 + SET CD_MFMT=%cd:\=/% + SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% + C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh + displayName: 'Install cygwin' + env: + CYGMIRROR: "http://mirror.easyname.at/cygwin" + +- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh + displayName: 'Install opam' + +- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh + displayName: 'Build Coq' + +- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh + displayName: 'Test Coq' diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 8489bcfc3a..fdbb0eca2b 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/README-developers.md b/dev/ci/README-developers.md index 6ca3aa2981..fa8962a06f 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -20,6 +20,9 @@ We are currently running tests on the following platforms: - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. +- Azure Pipelines is used to test the compilation of Coq and run the + test-suite on Windows. It is expected to replace appveyor eventually. + You can anticipate the results of most of these tests prior to submitting your PR by running GitLab CI on your private branches. To do so follow these steps: diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh new file mode 100755 index 0000000000..c0030c566f --- /dev/null +++ b/dev/ci/azure-build.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +set -e -x + +cd $(dirname $0)/../.. + +./configure -local +make -j 2 byte +make -j 2 world diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh new file mode 100755 index 0000000000..8a1e36659c --- /dev/null +++ b/dev/ci/azure-opam.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +set -e -x + +OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c + +wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz +tar -xf opam64.tar.xz +bash opam64/install.sh + +opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing +eval "$(opam env)" +opam install -y num ocamlfind ounit diff --git a/dev/ci/azure-test.sh b/dev/ci/azure-test.sh new file mode 100755 index 0000000000..8813245e5a --- /dev/null +++ b/dev/ci/azure-test.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +set -e -x + +#NB: if we make test-suite from the main makefile we get environment +#too large for exec error +cd $(dirname $0)/../../test-suite +make -j 2 clean +make -j 2 PRINT_LOGS=1 diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f1020e5f8e..baf470e021 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-12-05-V1" +# CACHEKEY: "bionic_coq-V2018-12-14-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.1 ounit.2.0.8 odoc.1.3.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh deleted file mode 100644 index b05d02c5be..0000000000 --- a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh +++ /dev/null @@ -1,14 +0,0 @@ -_OVERLAY_BRANCH=clean-transp-state - -if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - unicoq_CI_REF="$_OVERLAY_BRANCH" - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - - equations_CI_REF="$_OVERLAY_BRANCH" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - mtac2_CI_REF="$_OVERLAY_BRANCH" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - -fi diff --git a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh deleted file mode 100644 index 3600f1cd3e..0000000000 --- a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8705" ] || [ "$CI_BRANCH" = "vernac+remove_empty_hooks" ]; then - - elpi_CI_REF=vernac+remove_empty_hooks - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=vernac+remove_empty_hooks - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - paramcoq_CI_REF=vernac+remove_empty_hooks - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - plugin_tutorial_CI_REF=vernac+remove_empty_hooks - plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials - - mtac2_CI_REF=vernac+remove_empty_hooks - mtac2_CI_GITURL=https://github.com/ejgallego/mtac2 - -fi diff --git a/dev/ci/user-overlays/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh deleted file mode 100644 index 482792d7cd..0000000000 --- a/dev/ci/user-overlays/08850-poly-local-univs.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8850" ] || [ "$CI_BRANCH" = "poly-local-univs" ]; then - formal_topology_CI_REF=poly-local-univs - formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology - - paramcoq_CI_REF=poly-local-univs - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq -fi diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh deleted file mode 100644 index 17eb5fffae..0000000000 --- a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then - - Equations_CI_REF=program-hook-obligation-subst - Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh deleted file mode 100644 index 08112d3054..0000000000 --- a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then - - aactactics_CI_REF=ltac+use_atts_in_ast - aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - coqhammer_CI_REF=ltac+use_atts_in_ast - coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer - - Equations_CI_REF=ltac+use_atts_in_ast - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=ltac+use_atts_in_ast - mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh deleted file mode 100644 index 1c5157ba12..0000000000 --- a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then - - quickchick_CI_REF=lib+better_boot_coqproject - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh deleted file mode 100644 index e74e53fa40..0000000000 --- a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8933" ] || [ "$CI_BRANCH" = "solve-remaining-evars-initial-arg" ]; then - plugin_tutorial_CI_REF=solve-remaining-evars-initial-arg - plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials -fi diff --git a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh deleted file mode 100644 index d7130cc67a..0000000000 --- a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8985" ] || [ "$CI_BRANCH" = "build+pack_gramlib" ]; then - - elpi_CI_REF=use_coq_gramlib - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh deleted file mode 100644 index c8bea0c868..0000000000 --- a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then - - equations_CI_REF=legacy_proof_eng_clean - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh deleted file mode 100644 index 61ffa4a197..0000000000 --- a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then - - ltac2_CI_REF=vernac+move_extend_ast - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - -fi diff --git a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh deleted file mode 100644 index 14e7c0d7f0..0000000000 --- a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9051" ] || [ "$CI_BRANCH" = "camlp5-safe-api-strikes-back" ]; then - - equations_CI_REF=camlp5-safe-api-strikes-back - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - ltac2_CI_REF=camlp5-safe-api-strikes-back - ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 - -fi diff --git a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh deleted file mode 100644 index e9daa7a44e..0000000000 --- a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9065" ] || [ "$CI_BRANCH" = "gramlib+no_ploc" ]; then - - elpi_CI_REF=gramlib+no_ploc - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh new file mode 100644 index 0000000000..f532fdfc52 --- /dev/null +++ b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then + + ltac2_CI_REF=proof_rework + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + mtac2_CI_REF=proof_rework + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh new file mode 100644 index 0000000000..efcdd2e97f --- /dev/null +++ b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then + + paramcoq_CI_REF=stm-shallow-logic + paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq + +fi @@ -4,7 +4,9 @@ (release (flags :standard -rectypes) (ocamlopt_flags -O3 -unbox-closures)) (ireport (flags :standard -rectypes -w -9-27-40+60) - (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report))) + (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)) + (ocaml408 + (flags :standard -strict-sequence -strict-formats -short-paths -keep-locs -rectypes -w -9-27+40+60 -warn-error -5 -alert --deprecated))) ; The _ profile could help factoring the above, however it doesn't ; seem to work like we'd expect/like: diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index 521aff6bf6..8b0c736f50 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.ml @@ -11,7 +11,7 @@ (** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *) let error s = - prerr_endline ("fake_id: error: "^s); + prerr_endline ("fake_ide: error: "^s); exit 1 let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp @@ -22,7 +22,7 @@ type coqtop = { } let print_error msg = - Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg + Format.eprintf "fake_ide: error: @[%a@]\n%!" Pp.pp_with msg let base_eval_call ?(print=true) ?(fail=true) call coqtop = if print then prerr_endline (Xmlprotocol.pr_call call); @@ -257,10 +257,15 @@ let eval_print l coq = eval_call (wait ()) coq | [ Tok(_,"JOIN") ] -> eval_call (status true) coq + | [ Tok(_,"FAILJOIN") ] -> + after_fail coq (base_eval_call ~fail:false (status true) coq) | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" else prerr_endline "Good tip" + | [ Tok(_,"ABORT") ] -> + prerr_endline "Quitting fake_ide"; + exit 0 | Tok("#[^\n]*",_) :: _ -> () | _ -> error "syntax error" @@ -276,6 +281,8 @@ let grammar = ; Seq [Item (eat_rex "JOIN")] ; Seq [Item (eat_rex "GOALS")] ; Seq [Item (eat_rex "FAILGOALS")] + ; Seq [Item (eat_rex "FAILJOIN")] + ; Seq [Item (eat_rex "ABORT")] ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] ; Item (eat_rex "#[^\n]*") ] @@ -305,6 +312,8 @@ let main = Array.of_list (def_args @ ct), f | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in + prerr_endline ("Running: "^idetop_name^" "^ + (String.concat " " (Array.to_list coqtop_args))); let coq = let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in let ip = Xml_parser.make (Xml_parser.SChannel cin) in diff --git a/ide/idetop.ml b/ide/idetop.ml index 6a4c7603ee..716a942d5c 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -196,12 +196,24 @@ let process_goal sigma g = (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } -let export_pre_goals pgs = - { - Interface.fg_goals = pgs.Proof.fg_goals; - Interface.bg_goals = pgs.Proof.bg_goals; - Interface.shelved_goals = pgs.Proof.shelved_goals; - Interface.given_up_goals = pgs.Proof.given_up_goals +let process_goal_diffs diff_goal_map oldp nsigma ng = + let open Evd in + let og_s = match oldp with + | Some oldp -> + let Proof.{ sigma=osigma } = Proof.data oldp in + (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma } + with Not_found -> None) + | None -> None + in + let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in + { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } + +let export_pre_goals Proof.{ sigma; goals; stack; shelf; given_up } process = + let process = List.map (process sigma) in + { Interface.fg_goals = process goals + ; Interface.bg_goals = List.(map (fun (lg,rg) -> process lg, process rg)) stack + ; Interface.shelved_goals = process shelf + ; Interface.given_up_goals = process given_up } let goals () = @@ -212,22 +224,9 @@ let goals () = if Proof_diffs.show_diffs () then begin let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in let diff_goal_map = Proof_diffs.make_goal_map oldp newp in - - let process_goal_diffs nsigma ng = - let open Evd in - let og_s = match oldp with - | Some oldp -> - let (_,_,_,_,osigma) = Proof.proof oldp in - (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma } - with Not_found -> None) (* will appear as a new goal *) - | None -> None - in - let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in - { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } - in - Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs)) + Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp)) end else - Some (export_pre_goals (Proof.map_structured_proof newp process_goal)) + Some (export_pre_goals Proof.(data newp) process_goal) with Proof_global.NoCurrentProof -> None;; let evars () = @@ -235,7 +234,7 @@ let evars () = let doc = get_doc () in set_doc @@ Stm.finish ~doc; let pfts = Proof_global.give_me_the_proof () in - let all_goals, _, _, _, sigma = Proof.proof pfts in + let Proof.{ sigma } = Proof.data pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in @@ -245,8 +244,8 @@ let evars () = let hints () = try let pfts = Proof_global.give_me_the_proof () in - let all_goals, _, _, _, sigma = Proof.proof pfts in - match all_goals with + let Proof.{ goals; sigma } = Proof.data pfts in + match goals with | [] -> None | g :: _ -> let env = Goal.V82.env sigma g in diff --git a/ide/preferences.ml b/ide/preferences.ml index 045d650c1c..4aa8c92f73 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -815,33 +815,20 @@ let configure ?(apply=(fun () -> ())) parent = custom ~label box callback true in -(* - let show_toolbar = - bool - ~f:(fun s -> - current.show_toolbar <- s; - !show_toolbar s) - "Show toolbar" current.show_toolbar - in let window_height = string - ~f:(fun s -> current.window_height <- (try int_of_string s with _ -> 600); - !resize_window (); - ) - "Window height" - (string_of_int current.window_height) + ~f:(fun s -> try window_height#set (int_of_string s) with _ -> ()) + "Default window height at starting time" + (string_of_int window_height#get) in + let window_width = string - ~f:(fun s -> current.window_width <- - (try int_of_string s with _ -> 800)) - "Window width" - (string_of_int current.window_width) + ~f:(fun s -> try window_width#set (int_of_string s) with _ -> ()) + "Default window width at starting time" + (string_of_int window_width#get) in -*) -(* - let config_appearance = [show_toolbar; window_width; window_height] in -*) + let global_auto_revert = pbool "Enable global auto revert" global_auto_revert in let global_auto_revert_delay = string @@ -1049,10 +1036,7 @@ let configure ?(apply=(fun () -> ())) parent = Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; ]); -(* - Section("Appearance", - config_appearance); -*) + Section("Appearance", Some `PREFERENCES, [window_width; window_height]); Section("Externals", None, [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;cmd_editor;cmd_browse;doc_url;library_url]); diff --git a/interp/interp.mllib b/interp/interp.mllib index aa20bda705..147eaf20dc 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,6 +1,4 @@ Constrexpr -Genredexpr -Redops Tactypes Stdarg Notation_term diff --git a/interp/notation.ml b/interp/notation.ml index c866929234..b0854de4a3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1902,7 +1902,7 @@ let pr_visibility prglob = function (**********************************************************************) (* Synchronisation with reset *) -let freeze _ = +let freeze ~marshallable = (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope, !delimiters_map, !notations_key_table, !scope_class_map, !prim_token_interp_infos, !prim_token_uninterp_infos, @@ -1939,7 +1939,7 @@ let _ = Summary.init_function = init } let with_notation_protection f x = - let fs = freeze false in + let fs = freeze ~marshallable:false in try let a = f x in unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 7b01b6dc1c..bf3a8fe215 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -11,8 +11,6 @@ open Genarg open Geninterp -type 'a and_short_name = 'a * Names.lident option - let make0 ?dyn name = let wit = Genarg.make0 name in let () = register_val0 wit dyn in @@ -53,8 +51,6 @@ let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_red_expr = make0 "redexpr" - let wit_clause_dft_concl = make0 "clause_dft_concl" @@ -65,4 +61,3 @@ let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref let wit_clause = wit_clause_dft_concl -let wit_redexpr = wit_red_expr diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 5e5e43ed38..c974a4403c 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -14,15 +14,11 @@ open Loc open Names open EConstr open Libnames -open Genredexpr -open Pattern open Constrexpr open Genarg open Genintern open Locus -type 'a and_short_name = 'a * lident option - val wit_unit : unit uniform_genarg_type val wit_bool : bool uniform_genarg_type @@ -52,11 +48,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_red_expr : - ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, - (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type - val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type (** Aliases for compatibility *) @@ -66,7 +57,3 @@ val wit_preident : string uniform_genarg_type val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type -val wit_redexpr : - ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, - (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/kernel/dune b/kernel/dune index 4f2e0e4e28..01abdb8f67 100644 --- a/kernel/dune +++ b/kernel/dune @@ -18,3 +18,4 @@ ; warnings. (env (dev (flags :standard -w +a-4-44-50))) + ; (ocaml408 (flags :standard -w +a-3-4-44-50))) diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index c1a673edf0..171d51800e 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -57,7 +57,6 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * polymorphic * assumption_object_kind - type definition_kind = locality * polymorphic * definition_object_kind (** Kinds used in proofs *) diff --git a/library/declaremods.ml b/library/declaremods.ml index d20775a0d7..8699583cdf 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -845,7 +845,7 @@ end (** {6 Module operations handling summary freeze/unfreeze} *) let protect_summaries f = - let fs = Summary.freeze_summaries ~marshallable:`No in + let fs = Summary.freeze_summaries ~marshallable:false in try f fs with reraise -> (* Something wrong: undo the whole process *) diff --git a/library/global.ml b/library/global.ml index 67b00cf411..84d2a37170 100644 --- a/library/global.ml +++ b/library/global.ml @@ -36,10 +36,9 @@ let is_joined_environment () = let global_env_summary_tag = Summary.declare_summary_tag global_env_summary_name - { Summary.freeze_function = (function - | `Yes -> join_safe_environment (); !global_env - | `No -> !global_env - | `Shallow -> !global_env); + { Summary.freeze_function = (fun ~marshallable -> if marshallable then + (join_safe_environment (); !global_env) + else !global_env); unfreeze_function = (fun fr -> global_env := fr); init_function = (fun () -> global_env := Safe_typing.empty_environment) } diff --git a/library/goptions.ml b/library/goptions.ml index 340d74151b..1b907fd966 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -235,7 +235,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) let default = read() in let change = let _ = Summary.declare_summary (nickname key) - { Summary.freeze_function = (fun _ -> read ()); + { Summary.freeze_function = (fun ~marshallable -> read ()); Summary.unfreeze_function = write; Summary.init_function = (fun () -> write default) } in let cache_options (_,(l,m,v)) = diff --git a/library/lib.ml b/library/lib.ml index cce5feeb4a..d4381a6923 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -571,7 +571,7 @@ let open_section id = let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in if Nametab.exists_section obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); - let fs = Summary.freeze_summaries ~marshallable:`No in + let fs = Summary.freeze_summaries ~marshallable:false in add_entry (make_foname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); @@ -608,24 +608,21 @@ let close_section () = type frozen = lib_state -let freeze ~marshallable = - match marshallable with - | `Shallow -> - (* TASSI: we should do something more sensible here *) - let lib_stk = - CList.map_filter (function +let freeze ~marshallable = !lib_state + +let unfreeze st = lib_state := st + +let drop_objects st = + let lib_stk = + CList.map_filter (function | _, Leaf _ -> None | n, (CompilingLibrary _ as x) -> Some (n,x) | n, OpenedModule (it,e,op,_) -> - Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) + Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) | n, OpenedSection (op, _) -> - Some(n,OpenedSection(op,Summary.empty_frozen))) - !lib_state.lib_stk in - { !lib_state with lib_stk } - | _ -> - !lib_state - -let unfreeze st = lib_state := st + Some(n,OpenedSection(op,Summary.empty_frozen))) + st.lib_stk in + { st with lib_stk } let init () = unfreeze initial_lib_state; diff --git a/library/lib.mli b/library/lib.mli index d1b4977dd5..30569197bc 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -148,9 +148,12 @@ val close_section : unit -> unit type frozen -val freeze : marshallable:Summary.marshallable -> frozen +val freeze : marshallable:bool -> frozen val unfreeze : frozen -> unit +(** Keep only the libobject structure, not the objects themselves *) +val drop_objects : frozen -> frozen + val init : unit -> unit (** {6 Section management for discharge } *) diff --git a/library/states.ml b/library/states.ml index ae45b18b9c..92bdc410a3 100644 --- a/library/states.ml +++ b/library/states.ml @@ -13,8 +13,10 @@ open System type state = Lib.frozen * Summary.frozen +let lib_of_state = fst let summary_of_state = snd -let replace_summary (lib,_) s = lib, s +let replace_summary (lib,_) st = lib, st +let replace_lib (_,st) lib = lib, st let freeze ~marshallable = (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable) @@ -24,7 +26,7 @@ let unfreeze (fl,fs) = Summary.unfreeze_summaries fs let extern_state s = - System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes) + System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true) let intern_state s = unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); @@ -33,7 +35,7 @@ let intern_state s = (* Rollback. *) let with_state_protection f x = - let st = freeze ~marshallable:`No in + let st = freeze ~marshallable:false in try let a = f x in unfreeze st; a with reraise -> diff --git a/library/states.mli b/library/states.mli index 1e0361ea4f..52feb95222 100644 --- a/library/states.mli +++ b/library/states.mli @@ -19,11 +19,13 @@ val intern_state : string -> unit val extern_state : string -> unit type state -val freeze : marshallable:Summary.marshallable -> state +val freeze : marshallable:bool -> state val unfreeze : state -> unit val summary_of_state : state -> Summary.frozen +val lib_of_state : state -> Lib.frozen val replace_summary : state -> Summary.frozen -> state +val replace_lib : state -> Lib.frozen -> state (** {6 Rollback } *) diff --git a/library/summary.ml b/library/summary.ml index b68f1fb01b..8fbca44353 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -14,10 +14,8 @@ open Util module Dyn = Dyn.Make () -type marshallable = [ `Yes | `No | `Shallow ] - type 'a summary_declaration = { - freeze_function : marshallable -> 'a; + freeze_function : marshallable:bool -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit } @@ -31,7 +29,7 @@ let ml_modules = "ML-MODULES" let internal_declare_summary fadd sumname sdecl = let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in - let dyn_freeze b = infun (sdecl.freeze_function b) + let dyn_freeze ~marshallable = infun (sdecl.freeze_function ~marshallable) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in let ddecl = { @@ -70,9 +68,9 @@ type frozen = { let empty_frozen = { summaries = String.Map.empty; ml_module = None } let freeze_summaries ~marshallable : frozen = - let smap decl = decl.freeze_function marshallable in + let smap decl = decl.freeze_function ~marshallable in { summaries = String.Map.map smap !sum_map; - ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod; + ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod; } let warn_summary_out_of_scope = @@ -130,10 +128,10 @@ let remove_from_summary st tag = (** All-in-one reference declaration + registration *) -let ref_tag ?(freeze=fun _ r -> r) ~name x = +let ref_tag ?(freeze=fun ~marshallable r -> r) ~name x = let r = ref x in let tag = declare_summary_tag name - { freeze_function = (fun b -> freeze b !r); + { freeze_function = (fun ~marshallable -> freeze ~marshallable !r); unfreeze_function = ((:=) r); init_function = (fun () -> r := x) } in r, tag @@ -157,7 +155,7 @@ let (!) r = let ref ?(freeze=fun x -> x) ~name init = let r = Pervasives.ref (CEphemeron.create init, name) in declare_summary name - { freeze_function = (fun _ -> freeze !r); + { freeze_function = (fun ~marshallable -> freeze !r); unfreeze_function = ((:=) r); init_function = (fun () -> r := init) }; r diff --git a/library/summary.mli b/library/summary.mli index 64222761ba..0d77d725ac 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -11,15 +11,10 @@ (** This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) -type marshallable = - [ `Yes (* Full data will be marshalled to disk *) - | `No (* Full data will be store in memory, e.g. for Undo *) - | `Shallow ] (* Only part of the data will be marshalled to a slave process *) - (** Types of global Coq states. The ['a] type should be pure and marshallable by the standard OCaml marshalling function. *) type 'a summary_declaration = { - freeze_function : marshallable -> 'a; + freeze_function : marshallable:bool -> 'a; (** freeze_function [true] is for marshalling to disk. * e.g. lazy must be forced *) unfreeze_function : 'a -> unit; @@ -50,8 +45,8 @@ val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag The [init_function] restores the reference to its initial value. The [freeze_function] can be overridden *) -val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref -val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag +val ref : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref +val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag (* As [ref] but the value is local to a process, i.e. not sent to, say, proof * workers. It is useful to implement a local cache for example. *) @@ -81,7 +76,7 @@ val nop : unit -> unit type frozen val empty_frozen : frozen -val freeze_summaries : marshallable:marshallable -> frozen +val freeze_summaries : marshallable:bool -> frozen val unfreeze_summaries : ?partial:bool -> frozen -> unit val init_summaries : unit -> unit diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 923147ba2e..19ae97da77 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -553,7 +553,7 @@ type frozen_t = (grammar_entry * GramState.t) list * CLexer.keyword_state -let freeze _ : frozen_t = +let freeze ~marshallable : frozen_t = (!grammar_stack, CLexer.get_keyword_state ()) (* We compare the current state of the grammar and the state to unfreeze, @@ -586,7 +586,7 @@ let parser_summary_tag = Summary.init_function = Summary.nop } let with_grammar_rule_protection f x = - let fs = freeze false in + let fs = freeze ~marshallable:false in try let a = f x in unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 07f50f6cd5..4d817625f5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -164,11 +164,12 @@ module Btauto = struct let reify env t = lapp eval [|convert_env env; convert t|] - let print_counterexample p env gl = + let print_counterexample p penv gl = let var = lapp witness [|p|] in let var = EConstr.of_constr var in (* Compute an assignment that dissatisfies the goal *) - let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in + let redfun, _ = Redexpr.reduction_of_red_expr (Refiner.pf_env gl) Genredexpr.(CbvVm None) in + let _, var = redfun Refiner.(pf_env gl) Refiner.(project gl) var in let var = EConstr.Unsafe.to_constr var in let rec to_list l = match decomp_term (Tacmach.project gl) l with | App (c, _) @@ -192,7 +193,7 @@ module Btauto = struct let msg = try let var = to_list var in - let assign = List.combine env var in + let assign = List.combine penv var in let map_msg (key, v) = let b = if v then str "true" else str "false" in let sigma, env = Pfedit.get_current_context () in diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 37fc81ee38..ea86a4b514 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -132,7 +132,7 @@ let normalize_evaluables= open Ppconstr open Printer let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid -let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) +let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global let warn_deprecated_syntax = diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5d0d17ee6b..f9938c0356 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -492,7 +492,7 @@ type tcc_lemma_value = (* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in try f x with e -> let e = CErrors.push e in diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 156ee94a66..5d5d45c58f 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -314,7 +314,7 @@ END let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c -let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl +let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Pputils.pr_lident cl let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl let in_clause' = Pltac.in_clause diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 2267d43d93..5e3f4df192 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -22,8 +22,8 @@ open Tactypes open Locus open Decl_kinds open Genredexpr -open Pputils open Ppconstr +open Pputils open Printer open Genintern @@ -159,8 +159,8 @@ let string_of_genarg_arg (ArgumentType arg) = end | _ -> default - let pr_with_occurrences pr c = pr_with_occurrences pr keyword c - let pr_red_expr pr c = pr_red_expr pr keyword c + let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c + let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> @@ -186,12 +186,6 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c - let pr_or_by_notation f = CAst.with_val (function - | AN v -> f v - | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) - - let pr_located pr (_,x) = pr x - let pr_evaluable_reference = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) @@ -694,7 +688,7 @@ let pr_goal_selector ~toplevel s = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 0ab9e501bc..bc47036d92 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -98,8 +98,7 @@ val pr_may_eval : ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t -val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t -val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t +val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e626df5579..4bb52f599a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -632,7 +632,8 @@ let solve_remaining_by env sigma holes by = | Some evi -> let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in - let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in + let name, poly = Id.of_string "rewrite", false in + let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in Evd.define evk (EConstr.of_constr c) sigma in List.fold_left solve sigma indep diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 83f563e2ab..30e316b36d 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -270,7 +270,7 @@ constraint 'a = < type g_trm = Genintern.glob_constr_and_expr type g_pat = Genintern.glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference Stdarg.and_short_name or_var +type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -296,9 +296,6 @@ type glob_tactic_arg = (** Raw tactics *) -type r_trm = constr_expr -type r_pat = constr_pattern_expr -type r_cst = qualid or_by_notation type r_ref = qualid type r_nam = lident type r_lev = rlevel diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index da0ecfc449..8b6b14322b 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -269,7 +269,7 @@ constraint 'a = < type g_trm = Genintern.glob_constr_and_expr type g_pat = Genintern.glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference Stdarg.and_short_name or_var +type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -295,9 +295,6 @@ type glob_tactic_arg = (** Raw tactics *) -type r_trm = constr_expr -type r_pat = constr_pattern_expr -type r_cst = qualid or_by_notation type r_ref = qualid type r_nam = lident type r_lev = rlevel diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 284642b38c..816741b894 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2031,7 +2031,8 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in - let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in + let name, poly = Id.of_string "ltac_sub", false in + let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in GlobEnv.register_constr_interp0 wit_tactic eval diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 6d53349fa1..26202ef4ca 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -14,7 +14,6 @@ open Util open Pp open CAst open Names -open Nameops open Libnames open Pputils open Ppextend @@ -230,20 +229,6 @@ let tag_var = tag Tag.variable | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - let pr_lident {loc; v=id} = - match loc with - | None -> pr_id id - | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id) - - let pr_lname = function - | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) - | x -> pr_ast Name.print x - - let pr_or_var pr = function - | Locus.ArgArg x -> pr x - | Locus.ArgVar id -> pr_lident id - let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) | String s -> qs s diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index e7f71849a5..1cb3aa6d7a 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -21,11 +21,6 @@ val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t -val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t - -val pr_lident : lident -> Pp.t -val pr_lname : lname -> Pp.t - val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t val pr_com_at : int -> Pp.t val pr_sep_com : diff --git a/printing/pputils.ml b/printing/pputils.ml index 59e5f68f22..e6daf9544c 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -12,7 +12,6 @@ open Util open Pp open Genarg open Locus -open Genredexpr let beautify_comments = ref [] @@ -39,91 +38,25 @@ let pr_located pr (loc, x) = let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v) -let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar {CAst.v=s} -> Names.Id.print s - -let pr_with_occurrences pr keyword (occs,c) = - match occs with - | AllOccurrences -> - pr c - | NoOccurrences -> - failwith "pr_with_occurrences: no occurrences" - | OnlyOccurrences nl -> - hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - | AllOccurrencesBut nl -> - hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - -exception ComplexRedFlag - -let pr_short_red_flag pr r = - if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then - raise ComplexRedFlag - else if List.is_empty r.rConst then - if r.rDelta then mt () else raise ComplexRedFlag - else (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]") - -let pr_red_flag pr r = - try pr_short_red_flag pr r - with ComplexRedFlag -> - (if r.rBeta then pr_arg str "beta" else mt ()) ++ - (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else - (if r.rMatch then pr_arg str "match" else mt ()) ++ - (if r.rFix then pr_arg str "fix" else mt ()) ++ - (if r.rCofix then pr_arg str "cofix" else mt ())) ++ - (if r.rZeta then pr_arg str "zeta" else mt ()) ++ - (if List.is_empty r.rConst then - if r.rDelta then pr_arg str "delta" - else mt () - else - pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) - -let pr_union pr1 pr2 = function - | Inl a -> pr1 a - | Inr b -> pr2 b - -let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function - | Red false -> keyword "red" - | Hnf -> keyword "hnf" - | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) - ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o - | Cbv f -> - if f.rBeta && f.rMatch && f.rFix && f.rCofix && - f.rZeta && f.rDelta && List.is_empty f.rConst then - keyword "compute" - else - hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) - | Lazy f -> - hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f) - | Cbn f -> - hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f) - | Unfold l -> - hov 1 (keyword "unfold" ++ spc() ++ - prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l) - | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l) - | Pattern l -> - hov 1 (keyword "pattern" ++ - pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l) +let pr_lident { CAst.loc; v=id } = + let open Names.Id in + match loc with + | None -> print id + | Some loc -> let (b,_) = Loc.unloc loc in + pr_located print + (Some (Loc.make_loc (b,b + String.length (to_string id))), id) - | Red true -> - CErrors.user_err Pp.(str "Shouldn't be accessible from user.") - | ExtraRedExpr s -> - str s - | CbvVm o -> - keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o - | CbvNative o -> - keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o +let pr_lname = let open Names in function + | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) + | x -> pr_ast Name.print x -let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = - pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) +let pr_or_var pr = function + | ArgArg x -> pr x + | ArgVar id -> pr_lident id -let pr_or_by_notation f = let open Constrexpr in function - | {CAst.loc; v=AN v} -> f v - | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc +let pr_or_by_notation f = let open Constrexpr in CAst.with_val (function + | AN v -> f v + | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) let hov_if_not_empty n p = if Pp.ismt p then p else hov n p diff --git a/printing/pputils.mli b/printing/pputils.mli index 5b1969e232..ea554355bc 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -8,33 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Genarg -open Locus -open Genredexpr val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t (** Prints an object surrounded by its commented location *) -val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t +val pr_lident : lident -> Pp.t +val pr_lname : lname -> Pp.t +val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t -val pr_with_occurrences : - ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t - -val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t -val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t - -val pr_red_expr : - ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> - (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t - -val pr_red_expr_env : Environ.env -> Evd.evar_map -> - (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * - (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * - ('b -> Pp.t) * - (Environ.env -> Evd.evar_map -> 'c -> Pp.t) -> - (string -> Pp.t) -> - ('a,'b,'c) red_expr_gen -> Pp.t val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index b80133b171..be0139da06 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -546,10 +546,10 @@ let rec pr_evars_int_hd pr sigma i = function (hov 0 (pr i evk evi)) ++ (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest) -let pr_evars_int sigma ~shelf ~givenup i evs = +let pr_evars_int sigma ~shelf ~given_up i evs = let pr_status i = if List.mem i shelf then str " (shelved)" - else if List.mem i givenup then str " (given up)" + else if List.mem i given_up then str " (given up)" else mt () in pr_evars_int_hd (fun i evk evi -> @@ -761,7 +761,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else - let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in + let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in v 0 ((str "No more subgoals," ++ str " but there are non-instantiated existential variables:" ++ cut () ++ (hov 0 pei) @@ -789,7 +789,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = straightforward, but seriously, [Proof.proof] should return [evar_info]-s instead. *) let p = proof in - let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in + let Proof.{goals; stack; shelf; given_up; sigma} = Proof.data p in let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in let seeds = Proof.V82.top_evars p in begin match goals with @@ -821,7 +821,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in let os_map = match oproof with | Some op when diffs -> - let (_,_,_,_, osigma) = Proof.proof op in + let Proof.{sigma=osigma} = Proof.data op in let diff_goal_map = Proof_diffs.make_goal_map oproof proof in Some (osigma, diff_goal_map) | _ -> None @@ -834,8 +834,8 @@ let pr_open_subgoals ~proof = pr_open_subgoals_diff proof let pr_nth_open_subgoal ~proof n = - let gls,_,_,_,sigma = Proof.proof proof in - pr_subgoal n sigma gls + let Proof.{goals;sigma} = Proof.data proof in + pr_subgoal n sigma goals let pr_goal_by_id ~proof id = try diff --git a/printing/printer.mli b/printing/printer.mli index 357f30d1f4..fd4682a086 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -182,7 +182,7 @@ val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:Goal.goal list -> given_up:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index a381266976..b280ce909b 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -553,7 +553,7 @@ open Goal.Set let db_goal_map op np ng_to_og = let pr_goals title prf = Printf.printf "%s: " title; - let (goals,_,_,_,sigma) = Proof.proof prf in + let Proof.{goals;sigma} = Proof.data prf in List.iter (fun g -> Printf.printf "%d -> %s " (Evar.repr g) (goal_to_evar g sigma)) goals; let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in List.iter (fun g -> Printf.printf "%d " (Evar.repr g)) (elements gs); @@ -626,11 +626,11 @@ let make_goal_map_i op np = let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in let oevar_to_og = ref StringMap.empty in - let (_,_,_,_,osigma) = Proof.proof op in + let Proof.{sigma=osigma} = Proof.data op in List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og) (Goal.Set.elements rem_gs); - let (_,_,_,_,nsigma) = Proof.proof np in + let Proof.{sigma=nsigma} = Proof.data np in let get_og ng = let nevar = goal_to_evar ng nsigma in let oevar = StringMap.find nevar nevar_to_oevar in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index acf5510aa0..e2b7df19de 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -33,7 +33,7 @@ let () = CErrors.register_handler begin function end let get_nth_V82_goal p i = - let goals,_,_,_,sigma = Proof.proof p in + let Proof.{ sigma; goals } = Proof.data p in try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal @@ -120,7 +120,8 @@ let solve ?with_end_tac gi info_lvl tac pr = let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) let instantiate_nth_evar_com n com = - Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) + Proof_global.simple_with_current_proof (fun _ p -> + Proof.V82.instantiate_evar Global.(env ())n com p) (**********************************************************************) @@ -166,7 +167,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs -let refine_by_tactic env sigma ty tac = +let refine_by_tactic ~name ~poly env sigma ty tac = (* Save the initial side-effects to restore them afterwards. We set the current set of side-effects to be empty so that we can retrieve the ones created during the tactic invocation easily. *) @@ -175,7 +176,7 @@ let refine_by_tactic env sigma ty tac = (* Save the existing goals *) let prev_future_goals = save_future_goals sigma in (* Start a proof *) - let prf = Proof.start sigma [env, ty] in + let prf = Proof.start ~name ~poly sigma [env, ty] in let (prf, _) = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> @@ -184,9 +185,9 @@ let refine_by_tactic env sigma ty tac = iraise (e, info) in (* Plug back the retrieved sigma *) - let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in + let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in assert (stack = []); - let ans = match Proof.initial_goals prf with + let ans = match Proofview.initial_goals entry with | [c, _] -> c | _ -> assert false in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 155221947a..5699320af5 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -81,8 +81,13 @@ val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> EConstr.types -> unit Proofview.tactic -> constr * bool * UState.t -val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> - constr * Evd.evar_map +val refine_by_tactic + : name:Id.t + -> poly:bool + -> env -> Evd.evar_map + -> EConstr.types + -> unit Proofview.tactic + -> constr * Evd.evar_map (** A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may diff --git a/proofs/proof.ml b/proofs/proof.ml index 6c13c4946a..1aeb24606b 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -105,22 +105,29 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k) (* Subpart of the type of proofs. It contains the parts of the proof which are under control of the undo mechanism *) -type t = { - (* Current focused proofview *) - proofview: Proofview.proofview; - (* Entry for the proofview *) - entry : Proofview.entry; - (* History of the focusings, provides information on how - to unfocus the proof and the extra information stored while focusing. - The list is empty when the proof is fully unfocused. *) - focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list; - (* List of goals that have been shelved. *) - shelf : Goal.goal list; - (* List of goals that have been given up *) - given_up : Goal.goal list; - (* The initial universe context (for the statement) *) - initial_euctx : UState.t -} +type t = + { proofview: Proofview.proofview + (** Current focused proofview *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list + (** History of the focusings, provides information on how to unfocus + the proof and the extra information stored while focusing. The + list is empty when the proof is fully unfocused. *) + ; shelf : Goal.goal list + (** List of goals that have been shelved. *) + ; given_up : Goal.goal list + (** List of goals that have been given up *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** the name of the theorem whose proof is being constructed *) + ; poly : bool + (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) + } + +let initial_goals pf = Proofview.initial_goals pf.entry +let initial_euctx pf = pf.initial_euctx (*** General proof functions ***) @@ -141,7 +148,7 @@ let proof p = (goals,stack,shelf,given_up,sigma) type 'a pre_goals = { - fg_goals : 'a list; + fg_goals : 'a list; (** List of the focussed goals *) bg_goals : ('a list * 'a list) list; (** Zipper representing the unfocussed background goals *) @@ -311,7 +318,7 @@ let end_of_stack = CondEndStack end_of_stack_kind let unfocused = is_last_focus end_of_stack_kind -let start sigma goals = +let start ~name ~poly sigma goals = let entry, proofview = Proofview.init sigma goals in let pr = { proofview; @@ -320,9 +327,13 @@ let start sigma goals = shelf = [] ; given_up = []; initial_euctx = - Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in + Evd.evar_universe_context (snd (Proofview.proofview proofview)) + ; name + ; poly + } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr -let dependent_start goals = + +let dependent_start ~name ~poly goals = let entry, proofview = Proofview.dependent_init goals in let pr = { proofview; @@ -331,7 +342,10 @@ let dependent_start goals = shelf = [] ; given_up = []; initial_euctx = - Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in + Evd.evar_universe_context (snd (Proofview.proofview proofview)) + ; name + ; poly + } in let number_of_goals = List.length (Proofview.initial_goals pr.entry) in _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr @@ -375,9 +389,6 @@ let return ?pid (p : t) = let p = unfocus end_of_stack_kind p () in Proofview.return p.proofview -let initial_goals p = Proofview.initial_goals p.entry -let initial_euctx p = p.initial_euctx - let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in { p with proofview; entry } @@ -468,7 +479,7 @@ module V82 = struct { p with proofview = Proofview.V82.grab p.proofview } (* Main component of vernac command Existential *) - let instantiate_evar n com pr = + let instantiate_evar env n com pr = let tac = Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> let (evk, evi) = @@ -487,7 +498,7 @@ module V82 = struct let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma end in - let ((), proofview, _, _) = Proofview.apply (Global.env ()) tac pr.proofview in + let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in let shelf = List.filter begin fun g -> Evd.is_undefined (Proofview.return proofview) g @@ -507,3 +518,37 @@ let all_goals p = let set = add given_up set in let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in add bgoals set + +type data = + { sigma : Evd.evar_map + (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) + ; goals : Evar.t list + (** Focused goals *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; stack : (Evar.t list * Evar.t list) list + (** A representation of the focus stack *) + ; shelf : Evar.t list + (** A representation of the shelf *) + ; given_up : Evar.t list + (** A representation of the given up goals *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** The name of the theorem whose proof is being constructed *) + ; poly : bool + (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) + } + +let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } = + let goals, sigma = Proofview.proofview proofview in + (* spiwack: beware, the bottom of the stack is used by [Proof] + internally, and should not be exposed. *) + let rec map_minus_one f = function + | [] -> assert false + | [_] -> [] + | a::l -> f a :: (map_minus_one f l) + in + let stack = + map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in + { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly } diff --git a/proofs/proof.mli b/proofs/proof.mli index aaabea3454..fd5e905a3b 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -50,27 +50,70 @@ val proof : t -> * Goal.goal list * Goal.goal list * Evd.evar_map +[@@ocaml.deprecated "use [Proof.data]"] + +val initial_goals : t -> (EConstr.constr * EConstr.types) list +[@@ocaml.deprecated "use [Proof.data]"] + +val initial_euctx : t -> UState.t +[@@ocaml.deprecated "use [Proof.data]"] + +type data = + { sigma : Evd.evar_map + (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) + ; goals : Evar.t list + (** Focused goals *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; stack : (Evar.t list * Evar.t list) list + (** A representation of the focus stack *) + ; shelf : Evar.t list + (** A representation of the shelf *) + ; given_up : Evar.t list + (** A representation of the given up goals *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** The name of the theorem whose proof is being constructed *) + ; poly : bool; + (** polymorphism *) + } + +val data : t -> data (* Generic records structured like the return type of proof *) type 'a pre_goals = { fg_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the focussed goals *) bg_goals : ('a list * 'a list) list; + [@ocaml.deprecated "use [Proof.data]"] (** Zipper representing the unfocussed background goals *) shelved_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the goals on the shelf. *) given_up_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the goals that have been given up *) } +[@@ocaml.deprecated "use [Proof.data]"] -val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) - +(* needed in OCaml 4.05.0, not needed in newer ones *) +[@@@ocaml.warning "-3"] +val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"] +[@@ocaml.deprecated "use [Proof.data]"] +[@@@ocaml.warning "+3"] (*** General proof functions ***) -val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t -val dependent_start : Proofview.telescope -> t -val initial_goals : t -> (EConstr.constr * EConstr.types) list -val initial_euctx : t -> UState.t +val start + : name:Names.Id.t + -> poly:bool + -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t + +val dependent_start + : name:Names.Id.t + -> poly:bool + -> Proofview.telescope -> t (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) @@ -177,8 +220,9 @@ val no_focused_goal : t -> bool (* the returned boolean signal whether an unsafe tactic has been used. In which case it is [false]. *) -val run_tactic : Environ.env -> - unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) +val run_tactic + : Environ.env + -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) val maximal_unfocus : 'a focus_kind -> t -> t @@ -208,7 +252,8 @@ module V82 : sig val grab_evars : t -> t (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t + val instantiate_evar : + Environ.env -> int -> Constrexpr.constr_expr -> t -> t end (* returns the set of all goals in the proof *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 76a1e61ad2..8077da8807 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -90,14 +90,13 @@ type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator type pstate = { - pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Constr.named_context option; proof : Proof.t; - strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; universe_decl: UState.universe_decl; + strength : Decl_kinds.goal_kind; } type t = pstate list @@ -142,7 +141,7 @@ end (*** Proof Global manipulation ***) let get_all_proof_names () = - List.map (function { pid = id } -> id) !pstates + List.map Proof.(function pf -> (data pf.proof).name) !pstates let cur_pstate () = match !pstates with @@ -151,7 +150,7 @@ let cur_pstate () = let give_me_the_proof () = (cur_pstate ()).proof let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None -let get_current_proof_name () = (cur_pstate ()).pid +let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name let with_current_proof f = match !pstates with @@ -205,8 +204,12 @@ let check_no_pending_proof () = str"Use \"Abort All\" first or complete proof(s).") end +let pf_name_eq id ps = + let Proof.{ name } = Proof.data ps.proof in + Id.equal name id + let discard_gen id = - pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates + pstates := List.filter (fun pf -> not (pf_name_eq id pf)) !pstates let discard {CAst.loc;v=id} = let n = List.length !pstates in @@ -223,9 +226,9 @@ let discard_all () = pstates := [] (* [set_proof_mode] sets the proof mode to be used after it's called. It is typically called by the Proof Mode command. *) let set_proof_mode m id = - pstates := - List.map (function { pid = id' } as p -> - if Id.equal id' id then { p with mode = m } else p) !pstates; + pstates := List.map + (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps) + !pstates; update_proof_mode () let set_proof_mode mn = @@ -244,28 +247,26 @@ let disactivate_current_proof_mode () = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator = +let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator = let initial_state = { - pid = id; terminator = CEphemeron.create terminator; - proof = Proof.start sigma goals; + proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; endline_tactic = None; section_vars = None; - strength = str; mode = find_proof_mode "No"; - universe_decl = pl } in + universe_decl = pl; + strength = kind } in push initial_state pstates -let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator = +let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = let initial_state = { - pid = id; terminator = CEphemeron.create terminator; - proof = Proof.dependent_start goals; + proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; endline_tactic = None; section_vars = None; - strength = str; mode = find_proof_mode "No"; - universe_decl = pl } in + universe_decl = pl; + strength = kind } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars @@ -301,10 +302,10 @@ let set_used_variables l = ctx, [] let get_open_goals () = - let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in - List.length gl + + let Proof.{ goals; stack; shelf } = Proof.data (cur_pstate ()).proof in + List.length goals + List.fold_left (+) 0 - (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + + (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t @@ -323,12 +324,9 @@ let private_poly_univs = let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) = - let { pid; section_vars; strength; proof; terminator; universe_decl } = - cur_pstate () in + let { section_vars; proof; terminator; universe_decl; strength } = cur_pstate () in + let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in - let poly = pi2 strength (* Polymorphic *) in - let initial_goals = Proof.initial_goals proof in - let initial_euctx = Proof.initial_euctx proof in let constrain_variables ctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx in @@ -411,16 +409,16 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now const_entry_opaque = opaque; const_entry_universes = univs; } in - let entries = Future.map2 entry_fn fpl initial_goals in - { id = pid; entries = entries; persistence = strength; + let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in + { id = name; entries = entries; persistence = strength; universes }, fun pr_ending -> CEphemeron.get terminator pr_ending let return_proof ?(allow_partial=false) () = - let { pid; proof; strength = (_,poly,_) } = cur_pstate () in + let { proof } = cur_pstate () in if allow_partial then begin let proofs = Proof.partial_proof proof in - let _,_,_,_, evd = Proof.proof proof in + let Proof.{sigma=evd} = Proof.data proof in let eff = Evd.eval_side_effects evd in (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects @@ -428,7 +426,8 @@ let return_proof ?(allow_partial=false) () = let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd end else - let initial_goals = Proof.initial_goals proof in + let Proof.{name=pid;entry} = Proof.data proof in + let initial_goals = Proofview.initial_goals entry in let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in @@ -455,25 +454,23 @@ let set_terminator hook = module V82 = struct let get_current_initial_conclusions () = - let { pid; strength; proof } = cur_pstate () in - let initial = Proof.initial_goals proof in + let { proof; strength } = cur_pstate () in + let Proof.{ name; entry } = Proof.data proof in + let initial = Proofview.initial_goals entry in let goals = List.map (fun (o, c) -> c) initial in - pid, (goals, strength) + name, (goals, strength) end let freeze ~marshallable = - match marshallable with - | `Yes -> - CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") - | `Shallow -> !pstates - | `No -> !pstates + if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") + else !pstates let unfreeze s = pstates := s; update_proof_mode () let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof let copy_terminators ~src ~tgt = assert(List.length src = List.length tgt); List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt -let update_global_env () = +let update_global_env pf_info = with_current_proof (fun _ p -> Proof.in_proof p (fun sigma -> let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index d9c32cf9d5..9e904c57aa 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -135,7 +135,7 @@ module V82 : sig Decl_kinds.goal_kind) end -val freeze : marshallable:[`Yes | `No | `Shallow] -> t +val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t val copy_terminators : src:t -> tgt:t -> t diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index dbd5be23ab..0ce726db25 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -7,7 +7,6 @@ Logic Goal_select Proof_bullet Proof_global -Redexpr Refiner Tacmach Pfedit diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a5f691babb..df90354717 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -15,7 +15,6 @@ open Environ open Reductionops open Evd open Typing -open Redexpr open Tacred open Logic open Context.Named.Declaration @@ -71,11 +70,6 @@ let pf_global gls id = let sigma = project gls in Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id) -let pf_reduction_of_red_expr gls re c = - let (redfun, _) = reduction_of_red_expr (pf_env gls) re in - let sigma = project gls in - redfun (pf_env gls) sigma c - let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index ef6a1544e4..213ed7bfda 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,7 +12,6 @@ open Names open Constr open Environ open EConstr -open Redexpr open Locus (** Operations for handling terms under a local typing context. *) @@ -44,9 +43,6 @@ val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> Goal.goal sigma -> Id.t -val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr - - val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> Goal.goal sigma -> 'a -> Goal.goal sigma * 'b diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index b8af2bcd56..230a3207a8 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -49,12 +49,12 @@ let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not | `Valid (Some { Vernacstate.proof }) -> - let proof = Proof_global.proof_of_state proof in - let focused, r1, r2, r3, sigma = Proof.proof proof in - let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in - if List.for_all (fun x -> simple_goal sigma x rest) focused - then `Simple focused - else `Not + let proof = Proof_global.proof_of_state proof in + let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in + let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in + if List.for_all (fun x -> simple_goal sigma x rest) focused + then `Simple focused + else `Not type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] diff --git a/stm/stm.ml b/stm/stm.ml index e835bdcb1e..c84721bcb5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -78,7 +78,7 @@ let async_proofs_is_master opt = (* Protect against state changes *) let stm_purify f x = - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in try let res = f x in Vernacstate.unfreeze_interp_state st; @@ -343,7 +343,7 @@ module VCS : sig val set_ldir : Names.DirPath.t -> unit val get_ldir : unit -> Names.DirPath.t - val is_interactive : unit -> [`Yes | `No | `Shallow] + val is_interactive : unit -> bool val is_vio_doc : unit -> bool val current_branch : unit -> Branch.t @@ -543,8 +543,8 @@ end = struct (* {{{ *) let is_interactive () = match !doc_type with - | Interactive _ -> `Yes - | _ -> `No + | Interactive _ -> true + | _ -> false let is_vio_doc () = match !doc_type with @@ -632,13 +632,20 @@ end = struct (* {{{ *) " to "^Stateid.to_string block_stop^".")) in aux block_stop + (* [slice] copies a slice of the DAG, keeping only the last known valid state. + When it copies a state, it drops the libobjects and keeps only the structure. *) let slice ~block_start ~block_stop = let l = nodes_in_slice ~block_start ~block_stop in let copy_info v id = Vcs_.set_info v id { (get_info id) with state = Empty; vcs_backup = None,None } in + let make_shallow = function + | Valid st -> Valid (Vernacstate.make_shallow st) + | x -> x + in let copy_info_w_state v id = - Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in + let info = get_info id in + Vcs_.set_info v id { info with state = make_shallow info.state; vcs_backup = None,None } in let copy_proof_blockes v = let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in let props = @@ -750,7 +757,7 @@ end = struct (* {{{ *) end let print ?(now=false) () = - if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs) + if !Flags.debug then NB.command ~now (print_dag !vcs) let backup () = !vcs let restore v = vcs := v @@ -776,14 +783,14 @@ module State : sig val define : doc:doc -> ?safe_id:Stateid.t -> - ?redefine:bool -> ?cache:Summary.marshallable -> + ?redefine:bool -> ?cache:bool -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref val install_cached : Stateid.t -> unit - val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool - val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool + val is_cached : ?cache:bool -> Stateid.t -> bool + val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn @@ -832,16 +839,15 @@ end = struct (* {{{ *) Summary.project_from_summary st Util.(pi2 summary_pstate), Summary.project_from_summary st Util.(pi3 summary_pstate) - let freeze marshallable id = - VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) + let freeze ~marshallable id = + VCS.set_state id (Valid (Vernacstate.freeze_interp_state ~marshallable)) let freeze_invalid id iexn = VCS.set_state id (Error iexn) - let is_cached ?(cache=`No) id only_valid = + let is_cached ?(cache=false) id only_valid = if Stateid.equal id !cur_id then try match VCS.get_info id with - | { state = Empty } when cache = `Yes -> freeze `No id; true - | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true + | { state = Empty } when cache -> freeze ~marshallable:false id; true | _ -> true with VCS.Expired -> false else @@ -866,7 +872,7 @@ end = struct (* {{{ *) | _ -> (* coqc has a 1 slot cache and only for valid states *) - if VCS.is_interactive () = `No && Stateid.equal id !cur_id then () + if not (VCS.is_interactive ()) && Stateid.equal id !cur_id then () else anomaly Pp.(str "installing a non cached state.") let get_cached id = @@ -924,7 +930,7 @@ end = struct (* {{{ *) let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in e1 == e2 - let define ~doc ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) + let define ~doc ?safe_id ?(redefine=false) ?(cache=false) ?(feedback_processed=true) f id = feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id); @@ -933,13 +939,12 @@ end = struct (* {{{ *) anomaly Pp.(str"defining state "++str str_id++str" twice."); try stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ - if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); + if cache then "Y)" else "N)"); let good_id = match safe_id with None -> !cur_id | Some id -> id in fix_exn_ref := exn_on id ~valid:good_id; f (); fix_exn_ref := (fun x -> x); - if cache = `Yes then freeze `No id - else if cache = `Shallow then freeze `Shallow id; + if cache then freeze ~marshallable:false id; stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then @@ -958,14 +963,14 @@ end = struct (* {{{ *) | None, Some good_id -> (exn_on id ~valid:good_id (e, info)) | Some _, None -> (e, info) | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in - if cache = `Yes || cache = `Shallow then freeze_invalid id ie; + if cache then freeze_invalid id ie; Hooks.(call unreachable_state ~doc id ie); Exninfo.iraise ie let init_state = ref None let register_root_state () = - init_state := Some (Vernacstate.freeze_interp_state `No) + init_state := Some (Vernacstate.freeze_interp_state ~marshallable:false) let restore_root_state () = cur_id := Stateid.dummy; @@ -1178,7 +1183,7 @@ end = struct (* {{{ *) | _ -> None let undo_vernac_classifier v ~doc = - if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force + if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try match Vernacprop.under_control v with @@ -1508,9 +1513,7 @@ end = struct (* {{{ *) let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop = Future.create (State.exn_on id ~valid) (fun () -> let wall_clock1 = Unix.gettimeofday () in - if VCS.is_interactive () = `No - then Reach.known_state ~doc ~cache:`No eop - else Reach.known_state ~doc ~cache:`Shallow eop; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) eop; let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); @@ -1532,7 +1535,7 @@ end = struct (* {{{ *) * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in (* STATE: We use the current installed imperative state *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> let opaque = Proof_global.Opaque in @@ -1545,7 +1548,7 @@ end = struct (* {{{ *) let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator []) in - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; @@ -1676,7 +1679,7 @@ end = struct (* {{{ *) with VCS.Expired -> cur in aux stop in try - Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No stop; + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop; if drop then let _proof = Proof_global.return_proof ~allow_partial:true () in `OK_ADMITTED @@ -1689,14 +1692,14 @@ end = struct (* {{{ *) Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) - Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start; + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start; (* STATE SPEC: * - start: First non-expired state! [This looks very fishy] * - end : start + qed * => takes nothing from the itermediate states. *) (* STATE We use the state resulting from reaching start. *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); @@ -1934,9 +1937,9 @@ end = struct (* {{{ *) let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = Option.iter VCS.restore vcs; try - Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id; + Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id; stm_purify (fun () -> - let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in + let Proof.{sigma=sigma0} = Proof.data (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in let is_ground c = Evarutil.is_ground_term sigma0 c in if not ( @@ -1955,9 +1958,9 @@ end = struct (* {{{ *) * => captures state id in a future closure, which will discard execution state but for the proof + univs. *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp r_state_fb st ast); - let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in + let Proof.{sigma} = Proof.data (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> @@ -1994,12 +1997,12 @@ end = struct (* {{{ *) | VernacFail e -> find ~time ~batch ~fail:true e | e -> e, time, batch, fail in find ~time:false ~batch:false ~fail:false e in - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in Vernacentries.with_fail st fail (fun () -> (if time then System.with_time ~batch else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> - let goals, _, _, _, _ = Proof.proof p in + let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> let f, assign = @@ -2089,9 +2092,9 @@ end = struct (* {{{ *) let perform { r_where; r_doc; r_what; r_for } = VCS.restore r_doc; VCS.print (); - Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:`No r_where; + Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:false r_where; (* STATE *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in try (* STATE SPEC: * - start: r_where @@ -2133,14 +2136,14 @@ end (* }}} *) and Reach : sig val known_state : - doc:doc -> ?redefine_qed:bool -> cache:Summary.marshallable -> + doc:doc -> ?redefine_qed:bool -> cache:bool -> Stateid.t -> unit end = struct (* {{{ *) let async_policy () = - if Attributes.is_universe_polymorphism () then false - else if VCS.is_interactive () = `Yes then + if Attributes.is_universe_polymorphism () then false (* FIXME this makes no sense, it is the default value of the attribute *) + else if VCS.is_interactive () then (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy) else (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff) @@ -2322,7 +2325,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = * - end : maybe after recovery command. *) (* STATE: We use an updated state with proof *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in Option.iter (fun expr -> ignore(stm_vernac_interp id st { verbose = true; loc = None; expr; indentation = 0; strlen = 0 } )) @@ -2358,11 +2361,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let cherry_pick_non_pstate () = - let st = Summary.freeze_summaries ~marshallable:`No in + let st = Summary.freeze_summaries ~marshallable:false in let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in - st, Lib.freeze ~marshallable:`No in + st, Lib.freeze ~marshallable:false in let inject_non_pstate (s,l) = Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () @@ -2393,7 +2396,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } -> (fun () -> resilient_tactic id cblock (fun () -> - reach ~cache:`Shallow view.next; + reach ~cache:true view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch !cur_opt.async_proofs_n_tacworkers view.next id x) ), cache, true @@ -2406,39 +2409,39 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach view.next; (* State resulting from reach *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x) ); if eff then update_global_env () - ), (if eff then `Yes else cache), true + ), eff || cache, true | `Cmd { cast = x; ceff = eff } -> (fun () -> (match !cur_opt.async_proofs_mode with | APon | APonLazy -> resilient_command reach view.next | APoff -> reach view.next); - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); if eff then update_global_env () - ), (if eff then `Yes else cache), true + ), eff || cache, true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); wall_clock_last_fork := Unix.gettimeofday () - ), `Yes, true + ), true, true | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) - reach ~cache:`Shallow prev; + reach ~cache:true prev; reach view.next; (try - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in let info = Stateid.add info ~valid:prev id in Exninfo.iraise (e, info)); wall_clock_last_fork := Unix.gettimeofday () - ), `Yes, true + ), true, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function | `ASync (block_start, nodes, name, delegate) -> (fun () -> @@ -2468,7 +2471,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> - reach ~cache:`Shallow block_start; + reach ~cache:true block_start; let fp, cancel = if delegate then Slaves.build_proof ~doc @@ -2487,19 +2490,19 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~opaque ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id ~proof st x); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () - ), (if redefine_qed then `No else `Yes), true + ), not redefine_qed, true | `Sync (name, `Immediate) -> (fun () -> reach eop; - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); Proof_global.discard_all () - ), `Yes, true + ), true, true | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; reach eop; @@ -2523,25 +2526,25 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = if keep <> VtKeep VtKeepAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id ?proof st x); let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); Proof_global.discard_all () - ), `Yes, true + ), true, true | `MaybeASync (start, nodes, name, delegate) -> (fun () -> - reach ~cache:`Shallow start; + reach ~cache:true start; (* no sections *) if CList.is_empty (Environ.named_context (Global.env ())) then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) () else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) () - ), (if redefine_qed then `No else `Yes), true + ), not redefine_qed, true in aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); update_global_env () ), cache, true @@ -2551,8 +2554,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ), cache, true in let cache_step = - if !cur_opt.async_proofs_cache = Some Force then `Yes - else cache_step in + !cur_opt.async_proofs_cache = Some Force || cache_step + in State.define ~doc ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in @@ -2671,7 +2674,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = load_objs require_libs; (* We record the state at this point! *) - State.define ~doc ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; + State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); if async_proofs_is_master !cur_opt then begin @@ -2715,7 +2718,7 @@ let finish ~doc = ); doc let wait ~doc = - let doc = finish ~doc in + let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in Slaves.wait_all_done (); VCS.print (); doc @@ -2729,12 +2732,29 @@ let rec join_admitted_proofs id = join_admitted_proofs view.next | _ -> join_admitted_proofs view.next +(* Error resiliency may have tolerated some broken commands *) +let rec check_no_err_states ~doc visited id = + let open Stateid in + if Set.mem id visited then visited else + match state_of_id ~doc id with + | `Error e -> raise e + | _ -> + let view = VCS.visit id in + match view.step with + | `Qed(_,id) -> + let visited = check_no_err_states ~doc (Set.add id visited) id in + check_no_err_states ~doc visited view.next + | _ -> check_no_err_states ~doc (Set.add id visited) view.next + let join ~doc = let doc = wait ~doc in stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); stm_prerr_endline (fun () -> "Joining Admitted proofs"); - join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); + join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master); + stm_prerr_endline (fun () -> "Checking no error states"); + ignore(check_no_err_states ~doc (Stateid.Set.singleton Stateid.initial) + (VCS.get_branch_pos VCS.Branch.master)); VCS.print (); doc @@ -2785,7 +2805,7 @@ let merge_proof_branch ~valid ?id qast keep brname = VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname; VCS.delete_branch brname; VCS.gc (); - let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:`No qed_id in + let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:false qed_id in VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> @@ -2957,12 +2977,12 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in - let _st : unit = Reach.known_state ~doc ~cache:`Yes head_id in (* ensure it is ok *) + let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then @@ -2987,7 +3007,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) end; VCS.checkout_shallowest_proof_branch (); end in - State.define ~doc ~safe_id:head_id ~cache:`Yes step id; + State.define ~doc ~safe_id:head_id ~cache:true step id; Backtrack.record (); `Ok | VtUnknown, VtLater -> @@ -3116,7 +3136,7 @@ type focus = { let query ~doc ~at ~route s = stm_purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) - else Reach.known_state ~doc ~cache:`Yes at; + else Reach.known_state ~doc ~cache:true at; try while true do let { CAst.loc; v=ast } = parse_sentence ~doc at s in diff --git a/interp/genredexpr.ml b/tactics/genredexpr.ml index 607f2258fd..8209684c37 100644 --- a/interp/genredexpr.ml +++ b/tactics/genredexpr.ml @@ -63,3 +63,17 @@ type r_pat = constr_pattern_expr type r_cst = qualid or_by_notation type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen + +let make0 ?dyn name = + let wit = Genarg.make0 name in + let () = Geninterp.register_val0 wit dyn in + wit + +type 'a and_short_name = 'a * Names.lident option + +let wit_red_expr : + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, + (Genintern.glob_constr_and_expr,Names.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen, + (EConstr.t,Names.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen) + Genarg.genarg_type = + make0 "redexpr" diff --git a/tactics/hints.ml b/tactics/hints.ml index faff116af4..571ad9d160 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1516,8 +1516,8 @@ let pr_hint_term env sigma cl = let pr_applicable_hint () = let env = Global.env () in let pts = Proof_global.give_me_the_proof () in - let glss,_,_,_,sigma = Proof.proof pts in - match glss with + let Proof.{goals;sigma} = Proof.data pts in + match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> pr_hint_term env sigma (Goal.V82.concl sigma g) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index caf4c1eca3..356b43ec14 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -183,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = scheme on sort [sort]. Depending on the value of [dep_option] it will build a dependent lemma or a non-dependent one *) -let inversion_scheme env sigma t sort dep_option inv_op = +let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let (env,i) = add_prods_sign env sigma t in let ind = try find_rectype env sigma i @@ -201,7 +201,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = user_err ~hdr:"lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in + let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) @@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = invEnv ~init:Context.Named.empty end in let avoid = ref Id.Set.empty in - let _,_,_,_,sigma = Proof.proof pf in + let Proof.{sigma} = Proof.data pf in let sigma = Evd.minimize_universes sigma in let rec fill_holes c = match EConstr.kind sigma c with @@ -236,7 +236,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = p, sigma let add_inversion_lemma ~poly name env sigma t sort dep inv_op = - let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in + let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in let univs = Evd.const_univ_entry ~poly sigma in diff --git a/tactics/ppred.ml b/tactics/ppred.ml new file mode 100644 index 0000000000..dd1bcd4699 --- /dev/null +++ b/tactics/ppred.ml @@ -0,0 +1,83 @@ +open Util +open Pp +open Locus +open Genredexpr +open Pputils + +let pr_with_occurrences pr keyword (occs,c) = + match occs with + | AllOccurrences -> + pr c + | NoOccurrences -> + failwith "pr_with_occurrences: no occurrences" + | OnlyOccurrences nl -> + hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + | AllOccurrencesBut nl -> + hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + +exception ComplexRedFlag + +let pr_short_red_flag pr r = + if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then + raise ComplexRedFlag + else if List.is_empty r.rConst then + if r.rDelta then mt () else raise ComplexRedFlag + else (if r.rDelta then str "-" else mt ()) ++ + hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]") + +let pr_red_flag pr r = + try pr_short_red_flag pr r + with ComplexRedFlag -> + (if r.rBeta then pr_arg str "beta" else mt ()) ++ + (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else + (if r.rMatch then pr_arg str "match" else mt ()) ++ + (if r.rFix then pr_arg str "fix" else mt ()) ++ + (if r.rCofix then pr_arg str "cofix" else mt ())) ++ + (if r.rZeta then pr_arg str "zeta" else mt ()) ++ + (if List.is_empty r.rConst then + if r.rDelta then pr_arg str "delta" + else mt () + else + pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ + hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) + +let pr_union pr1 pr2 = function + | Inl a -> pr1 a + | Inr b -> pr2 b + +let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function + | Red false -> keyword "red" + | Hnf -> keyword "hnf" + | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) + ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o + | Cbv f -> + if f.rBeta && f.rMatch && f.rFix && f.rCofix && + f.rZeta && f.rDelta && List.is_empty f.rConst then + keyword "compute" + else + hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) + | Lazy f -> + hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f) + | Cbn f -> + hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f) + | Unfold l -> + hov 1 (keyword "unfold" ++ spc() ++ + prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l) + | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l) + | Pattern l -> + hov 1 (keyword "pattern" ++ + pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l) + + | Red true -> + CErrors.user_err Pp.(str "Shouldn't be accessible from user.") + | ExtraRedExpr s -> + str s + | CbvVm o -> + keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o + | CbvNative o -> + keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o + +let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = + pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) diff --git a/tactics/ppred.mli b/tactics/ppred.mli new file mode 100644 index 0000000000..b3a306a36f --- /dev/null +++ b/tactics/ppred.mli @@ -0,0 +1,19 @@ +open Genredexpr + +val pr_with_occurrences : + ('a -> Pp.t) -> (string -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t + +val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t +val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t + +val pr_red_expr : + ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t + +val pr_red_expr_env : Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * + (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * + ('b -> Pp.t) * + (Environ.env -> Evd.evar_map -> 'c -> Pp.t) -> + (string -> Pp.t) -> + ('a,'b,'c) red_expr_gen -> Pp.t diff --git a/proofs/redexpr.ml b/tactics/redexpr.ml index 6658c37f41..aabfae444e 100644 --- a/proofs/redexpr.ml +++ b/tactics/redexpr.ml @@ -74,13 +74,13 @@ let set_strategy_one ref l = Csymtable.set_opaque_const sp | ConstKey sp, _ -> let cb = Global.lookup_constant sp in - (match cb.const_body with - | OpaqueDef _ -> + (match cb.const_body with + | OpaqueDef _ -> user_err ~hdr:"set_transparent_const" (str "Cannot make" ++ spc () ++ Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ - spc () ++ str "transparent because it was declared opaque."); - | _ -> Csymtable.set_transparent_const sp) + spc () ++ str "transparent because it was declared opaque."); + | _ -> Csymtable.set_transparent_const sp) | _ -> () let cache_strategy (_,str) = @@ -126,10 +126,10 @@ type strategy_obj = let inStrategy : strategy_obj -> obj = declare_object {(default_object "STRATEGY") with cache_function = (fun (_,obj) -> cache_strategy obj); - load_function = (fun _ (_,obj) -> cache_strategy obj); - subst_function = subst_strategy; + load_function = (fun _ (_,obj) -> cache_strategy obj); + subst_function = subst_strategy; discharge_function = discharge_strategy; - classify_function = classify_strategy } + classify_function = classify_strategy } let set_strategy local str = @@ -154,16 +154,16 @@ let make_flag env f = let red = if f.rDelta then (* All but rConst *) let red = red_add red fDELTA in - let red = red_add_transparent red + let red = red_add_transparent red (Conv_oracle.get_transp_state (Environ.oracle env)) in - List.fold_right - (fun v red -> red_sub red (make_flag_constant v)) - f.rConst red + List.fold_right + (fun v red -> red_sub red (make_flag_constant v)) + f.rConst red else (* Only rConst *) let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in - List.fold_right - (fun v red -> red_add red (make_flag_constant v)) - f.rConst red + List.fold_right + (fun v red -> red_add red (make_flag_constant v)) + f.rConst red in red (* table of custom reductino fonctions, not synchronized, @@ -234,7 +234,7 @@ let reduction_of_red_expr env = let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in let () = if not (!simplIsCbn || List.is_empty f.rConst) then - warn_simpl_unfolding_modifiers () in + warn_simpl_unfolding_modifiers () in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) | Cbn f -> @@ -246,9 +246,9 @@ let reduction_of_red_expr env = | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> - (try reduction_of_red_expr (String.Map.find s !red_expr_tab) - with Not_found -> - user_err ~hdr:"Redexpr.reduction_of_red_expr" + (try reduction_of_red_expr (String.Map.find s !red_expr_tab) + with Not_found -> + user_err ~hdr:"Redexpr.reduction_of_red_expr" (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) @@ -270,9 +270,9 @@ let inReduction : bool * string * red_expr -> obj = cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e); load_function = (fun _ (_,(_,s,e)) -> decl_red_expr s e); subst_function = - (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e); + (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e); classify_function = - (fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) } + (fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) } let declare_red_expr locality s expr = Lib.add_anonymous_leaf (inReduction (locality,s,expr)) diff --git a/proofs/redexpr.mli b/tactics/redexpr.mli index 1e59f436c3..1f65862701 100644 --- a/proofs/redexpr.mli +++ b/tactics/redexpr.mli @@ -20,7 +20,7 @@ open Locus type red_expr = (constr, evaluable_global_reference, constr_pattern) red_expr_gen - + val out_with_occurrences : 'a with_occurrences -> occurrences * 'a val reduction_of_red_expr : diff --git a/interp/redops.ml b/tactics/redops.ml index b9a74136e4..6f83ea9a34 100644 --- a/interp/redops.ml +++ b/tactics/redops.ml @@ -21,14 +21,14 @@ let make_red_flag l = | FCofix :: lf -> add_flag { red with rCofix = true } lf | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> - if red.rDelta then - CErrors.user_err Pp.(str - "Cannot set both constants to unfold and constants not to unfold"); + if red.rDelta then + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> - if red.rConst <> [] && not red.rDelta then - CErrors.user_err Pp.(str - "Cannot set both constants to unfold and constants not to unfold"); + if red.rConst <> [] && not red.rDelta then + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l; rDelta = true } lf diff --git a/interp/redops.mli b/tactics/redops.mli index 7254f29b25..7254f29b25 100644 --- a/interp/redops.mli +++ b/tactics/redops.mli diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5b1d7dabba..b1f2ceee57 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -889,7 +889,7 @@ let reduce redexp cl = let trace env sigma = let open Printer in let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in - Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp)) + Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp)) in let trace () = let sigma, env = Pfedit.get_current_context () in diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 5afec74fae..1861c5b99b 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -6,6 +6,10 @@ Hipattern Ind_tables Eqschemes Elimschemes +Genredexpr +Redops +Redexpr +Ppred Tactics Abstract Elim diff --git a/test-suite/Makefile b/test-suite/Makefile index 9d2277c37e..34a1900bbc 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -90,19 +90,17 @@ FAIL = >&2 echo 'FAILED $@' # Testing subsystems ####################################################################### -# Apart so that it can be easily skipped with overriding +# These targets can be skipped by doing `make TARGET= test-suite` COMPLEXITY := $(if $(bogomips),complexity) - BUGS := bugs/opened bugs/closed - INTERACTIVE := interactive - +UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc ssr # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ @@ -119,6 +117,10 @@ PREREQUISITELOG = prerequisite/admit.v.log \ all: run $(MAKE) report +# do nothing +.PHONY: noop +noop: ; + run: $(SUBSYSTEMS) bugs: $(BUGS) @@ -569,7 +571,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ + $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/dune b/test-suite/dune index c5fa0bb14a..eae072553a 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -70,4 +70,4 @@ (progn ; XXX: we will allow to set the NJOBS variable in a future Dune ; version, either by using an env var or by letting Dune set `-j` - (run make -j 2 BIN= PRINT_LOGS=1)))) + (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests})))) diff --git a/test-suite/ide/join-sync.fake b/test-suite/ide/join-sync.fake new file mode 100644 index 0000000000..236028ce46 --- /dev/null +++ b/test-suite/ide/join-sync.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency + async proofs off +# coq-prog-args: ("-async-proofs" "off" "-async-proofs-command-error-resilience" "on") +# + +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +WAIT +FAILJOIN +ASSERT TIP here +ABORT diff --git a/test-suite/ide/join.fake b/test-suite/ide/join.fake new file mode 100644 index 0000000000..c4c696ad9a --- /dev/null +++ b/test-suite/ide/join.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency +# + +ADD { Section x. } +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +ADD { End x. } +FAILJOIN +ASSERT TIP here +ABORT diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 5cf2157044..e58b9ccac7 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -323,7 +323,8 @@ let loop_flush_all () = let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 let evleq e1 e2 = CList.equal Evar.equal e1 e2 let cproof p1 p2 = - let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in + let Proof.{goals=a1;stack=a2;shelf=a3;given_up=a4} = Proof.data p1 in + let Proof.{goals=b1;stack=b2;shelf=b3;given_up=b4} = Proof.data p2 in evleq a1 b1 && CList.equal (pequal evleq evleq) a2 b2 && CList.equal Evar.equal a3 b3 && diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1a6eda446c..8f155adb8a 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -483,7 +483,7 @@ let save_proof ?proof = function let pftree = Proof_global.give_me_the_proof () in let id, k, typ = Pfedit.current_proof_statement () in let typ = EConstr.Unsafe.to_constr typ in - let universes = Proof.initial_euctx pftree in + let universes = Proof.((data pftree).initial_euctx) in (* This will warn if the proof is complete *) let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 790b62c9d0..4e79b50b79 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1359,7 +1359,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze ~marshallable:`No in + let fs = Lib.freeze ~marshallable:false in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 3620e177fe..8d6268753e 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -394,7 +394,7 @@ let unfreeze_ml_modules x = let _ = Summary.declare_ml_modules_summary - { Summary.freeze_function = (fun _ -> get_loaded_modules ()); + { Summary.freeze_function = (fun ~marshallable -> get_loaded_modules ()); Summary.unfreeze_function = unfreeze_ml_modules; Summary.init_function = reset_loaded_modules } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 8535585749..e0dd3380f9 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -700,7 +700,7 @@ open Pputils | None -> mt() | Some r -> keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ + Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ keyword " in" ++ spc() in let pr_def_body = function @@ -1134,7 +1134,7 @@ open Pputils let pr_mayeval r c = match r with | Some r0 -> hov 2 (keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in @@ -1146,7 +1146,7 @@ open Pputils | VernacDeclareReduction (s,r) -> return ( keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r ) | VernacPrint p -> return (pr_printable p) diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index f26e0d0885..a647b2ef73 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -52,4 +52,4 @@ let set_command_entry e = Vernac_.command_entry_ref := e let get_command_entry () = !Vernac_.command_entry_ref let () = - register_grammar Stdarg.wit_red_expr (Vernac_.red_expr); + register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr); diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c6c6f74152..e6e3db4beb 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -82,12 +82,12 @@ let show_proof () = let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in - let gls,_,shelf,givenup,sigma = Proof.proof pfts in - pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma) + let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in + pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma) let show_universes () = let pfts = Proof_global.give_me_the_proof () in - let gls,_,_,_,sigma = Proof.proof pfts in + let Proof.{goals;sigma} = Proof.data pfts in let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx @@ -96,9 +96,9 @@ let show_universes () = let show_intro all = let open EConstr in let pf = Proof_global.give_me_the_proof() in - let gls,_,_,_,sigma = Proof.proof pf in - if not (List.is_empty gls) then begin - let gl = {Evd.it=List.hd gls ; sigma = sigma; } in + let Proof.{goals;sigma} = Proof.data pf in + if not (List.is_empty goals) then begin + let gl = {Evd.it=List.hd goals ; sigma = sigma; } in let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in @@ -1047,8 +1047,9 @@ let vernac_set_end_tac tac = let vernac_set_used_variables e = let env = Global.env () in + let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in let tys = - List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in + List.map snd (initial_goals (Proof_global.give_me_the_proof ())) in let tys = List.map EConstr.Unsafe.to_constr tys in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in @@ -1815,8 +1816,8 @@ let vernac_global_check c = let get_nth_goal n = let pf = Proof_global.give_me_the_proof() in - let gls,_,_,_,sigma = Proof.proof pf in - let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in + let Proof.{goals;sigma} = Proof.data pf in + let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in gl exception NoHyp @@ -2435,7 +2436,7 @@ let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; try interp ?verbosely ?proof ~st cmd; - Vernacstate.freeze_interp_state `No + Vernacstate.freeze_interp_state ~marshallable:false with exn -> let exn = CErrors.push exn in Vernacstate.invalidate_cache (); diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index aa8bcdc328..b40bccf27e 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -33,11 +33,18 @@ let do_if_not_cached rf f v = | Some _ -> () -let freeze_interp_state marshallable = +let freeze_interp_state ~marshallable = { system = update_cache s_cache (States.freeze ~marshallable); proof = update_cache s_proof (Proof_global.freeze ~marshallable); - shallow = marshallable = `Shallow } + shallow = marshallable } let unfreeze_interp_state { system; proof } = do_if_not_cached s_cache States.unfreeze system; do_if_not_cached s_proof Proof_global.unfreeze proof + +let make_shallow st = + let lib = States.lib_of_state st.system in + { st with + system = States.replace_lib st.system @@ Lib.drop_objects lib; + shallow = true; + } diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b4d478d12d..ed20cb935a 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -14,8 +14,10 @@ type t = { shallow : bool (* is the state trimmed down (libstack) *) } -val freeze_interp_state : Summary.marshallable -> t +val freeze_interp_state : marshallable:bool -> t val unfreeze_interp_state : t -> unit +val make_shallow : t -> t + (* WARNING: Do not use, it will go away in future releases *) val invalidate_cache : unit -> unit |