diff options
69 files changed, 1692 insertions, 1155 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a6b17fd148..dae412923b 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-09-24-V01" + CACHEKEY: "bionic_coq-V2018-09-25-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -419,6 +419,9 @@ ci-mtac2: ci-pidetop: <<: *ci-template +ci-plugin-tutorial: + <<: *ci-template + ci-quickchick: <<: *ci-template-flambda diff --git a/.travis.yml b/.travis.yml index 1a2c909c7d..52e5e051d2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -37,15 +37,15 @@ addons: env: global: - NJOBS=2 - # system is == 4.02.3 - - COMPILER="system" + - COMPILER="4.05.0" - COMPILER_BE="4.07.0" - DUNE_VER=".1.1.1" - - CAMLP5_VER=".6.14" + - CAMLP5_VER=".7.01" - CAMLP5_VER_BE=".7.06" - - FINDLIB_VER=".1.4.1" + # ounit forces FINDLIB here + - FINDLIB_VER=".1.7.3" - FINDLIB_VER_BE=".1.8.0" - - LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2" + - LABLGTK="lablgtk.2.18.6 conf-gtksourceview.2" - LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2" - NATIVE_COMP="yes" - COQ_DEST="-local" @@ -56,13 +56,13 @@ matrix: include: - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" EXTRA_OPAM="ounit" + - TEST_TARGET="test-suite" COMPILER="4.05.0+32bit" EXTRA_OPAM="ounit" - if: NOT (type = pull_request) env: - TEST_TARGET="validate" TW="travis_wait" - if: NOT (type = pull_request) env: - - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" + - TEST_TARGET="validate" COMPILER="4.05.0+32bit" TW="travis_wait" - if: NOT (type = pull_request) env: - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" @@ -1,5 +1,10 @@ -Changes beyond 8.9 -================== +Changes from 8.9 to 8.10 +======================== + +OCaml + +- Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the + INSTALL file for more information on dependencies. Plugins @@ -180,6 +185,8 @@ Vernacular Commands scope. If you want the previous behavior, use `Global Set SsrHave NoTCResolution`. - Multiple sections with the same name are allowed. +- Combined Scheme can now work when inductive schemes are generated in sort + Type. It used to be limited to sort Prop. Coq binaries and process model @@ -29,7 +29,7 @@ WHAT DO YOU NEED ? To compile Coq yourself, you need: - - OCaml (version >= 4.02.3) + - OCaml (version >= 4.05.0) (available at https://ocaml.org/) (This version of Coq has been tested up to OCaml 4.07.0) @@ -39,7 +39,7 @@ WHAT DO YOU NEED ? - Findlib (version >= 1.4.1) (available at http://projects.camlcity.org/projects/findlib.html) - - Camlp5 (version >= 6.14) + - Camlp5 (version >= 7.01) (available at https://camlp5.github.io/) - GNU Make version 3.81 or later @@ -88,7 +88,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). computer and that "ocamlc" (or, better, its native code version "ocamlc.opt") lies in a directory which is present in your $PATH environment variable. At the time of writing this sentence, all - versions of Objective Caml later or equal to 4.02.3 are + versions of Objective Caml later or equal to 4.05.0 are supported. To get Coq in native-code, (it runs 4 to 10 times faster than diff --git a/Makefile.ci b/Makefile.ci index e86504b76d..7fdcb35bc9 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -34,6 +34,7 @@ CI_TARGETS=ci-bedrock2 \ ci-math-comp \ ci-mtac2 \ ci-pidetop \ + ci-plugin-tutorial \ ci-quickchick \ ci-sf \ ci-simple-io \ diff --git a/configure.ml b/configure.ml index e3437a1d5b..a508ac6071 100644 --- a/configure.ml +++ b/configure.ml @@ -609,14 +609,14 @@ let caml_version_nums = "Is it installed properly?") let check_caml_version () = - if caml_version_nums >= [4;2;3] then + if caml_version_nums >= [4;5;0] then cprintf "You have OCaml %s. Good!" caml_version else let () = cprintf "Your version of OCaml is %s." caml_version in if !prefs.force_caml_version then warn "Your version of OCaml is outdated." else - die "You need OCaml 4.02.3 or later." + die "You need OCaml 4.05.0 or later." let _ = check_caml_version () @@ -656,16 +656,12 @@ let camltag = match caml_version_list with 45: "open" shadowing a label or constructor: see 44 48: implicit elimination of optional arguments: too common 50: unexpected documentation comment: too common and annoying to avoid - 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9 *) let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58" let coq_warn_error = if !prefs.warn_error then "-warn-error +a" - ^ (if caml_version_nums > [4;2;3] - then "-56" - else "") else "" (* Flags used to compile Coq and plugins (via coq_makefile) *) @@ -1054,7 +1050,7 @@ let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout try Some (Sys.getenv "COQ_CONFIGURE_PREFIX") with | Not_found when !prefs.interactive -> None - | Not_found -> Some "_build/default/install" + | Not_found -> Some "_build/install/default" end | p -> p in match uservalue, env_prefix with diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 181c43615b..956a916792 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -11,7 +11,7 @@ type loc = { loc_end : Lexing.position; } -type code = { code : string } +type code = { code : string; loc : loc; } type user_symbol = | Ulist1 of user_symbol diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index bfa4e2b57b..81a53e887b 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -29,6 +29,7 @@ let newline lexbuf = let num_comments = ref 0 let num_braces = ref 0 +let ocaml_start_pos = ref Lexing.dummy_pos let mode () = if !num_braces = 0 then Extend else OCaml @@ -57,10 +58,10 @@ let end_comment lexbuf = else None -let start_ocaml _ = +let start_ocaml lexbuf = let () = match mode () with | OCaml -> Buffer.add_string ocaml_buf "{" - | Extend -> () + | Extend -> ocaml_start_pos := lexeme_start_p lexbuf in incr num_braces @@ -70,7 +71,11 @@ let end_ocaml lexbuf = else if !num_braces = 0 then let s = Buffer.contents ocaml_buf in let () = Buffer.reset ocaml_buf in - Some (CODE { Coqpp_ast.code = s }) + let loc = { + Coqpp_ast.loc_start = !ocaml_start_pos; + Coqpp_ast.loc_end = lexeme_end_p lexbuf + } in + Some (CODE { Coqpp_ast.code = s; loc }) else let () = Buffer.add_string ocaml_buf "}" in None @@ -87,7 +92,7 @@ let number = [ '0'-'9' ] rule extend = parse | "(*" { start_comment (); comment lexbuf } -| "{" { start_ocaml (); ocaml lexbuf } +| "{" { start_ocaml lexbuf; ocaml lexbuf } | "GRAMMAR" { GRAMMAR } | "VERNAC" { VERNAC } | "TACTIC" { TACTIC } @@ -127,7 +132,7 @@ rule extend = parse | eof { EOF } and ocaml = parse -| "{" { start_ocaml (); ocaml lexbuf } +| "{" { start_ocaml lexbuf; ocaml lexbuf } | "}" { match end_ocaml lexbuf with Some tk -> tk | None -> ocaml lexbuf } | '\n' { newline lexbuf; Buffer.add_char ocaml_buf '\n'; ocaml lexbuf } | '\"' { Buffer.add_char ocaml_buf '\"'; ocaml_string lexbuf } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index a8ed95f5ba..d9fff46d88 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -21,6 +21,13 @@ let pr_loc loc = let epos = loc.loc_end.pos_cnum - loc.loc_start.pos_bol in Printf.sprintf "File \"%s\", line %d, characters %d-%d:" file line bpos epos +let print_code fmt c = + let loc = c.loc.loc_start in + (** Print the line location as a source annotation *) + let padding = String.make (loc.pos_cnum - loc.pos_bol + 1) ' ' in + let code_insert = asprintf "\n# %i \"%s\"\n%s%s" loc.pos_lnum loc.pos_fname padding c.code in + fprintf fmt "@[@<0>%s@]@\n" code_insert + let parse_file f = let chan = open_in f in let lexbuf = Lexing.from_channel chan in @@ -181,8 +188,7 @@ let print_fun fmt (vars, body) = in let () = fprintf fmt "fun@ " in let () = List.iter iter vars in - (* FIXME: use Coq locations in the macros *) - let () = fprintf fmt "loc ->@ @[%s@]" body.code in + let () = fprintf fmt "loc ->@ @[%a@]" print_code body in () (** Meta-program instead of calling Tok.of_pattern here because otherwise @@ -304,8 +310,8 @@ let rec print_binders fmt = function fprintf fmt "%s@ %a" id print_binders rem let print_rule fmt r = - fprintf fmt "@[TyML (%a, @[fun %a -> %s@])@]" - print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code + fprintf fmt "@[TyML (%a, @[fun %a -> %a@])@]" + print_clause r.tac_toks print_binders r.tac_toks print_code r.tac_body let rec print_rules fmt = function | [] -> () @@ -338,7 +344,7 @@ let declare_plugin fmt name = fprintf fmt "let _ = Mltop.add_known_module %s@\n" plugin_name let pr_ast fmt = function -| Code s -> fprintf fmt "%s@\n" s.code +| Code s -> fprintf fmt "%a@\n" print_code s | Comment s -> fprintf fmt "%s@\n" s | DeclarePlugin name -> declare_plugin fmt name | GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram diff --git a/default.nix b/default.nix index 29c0c68174..1faaafae03 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/52a1179b6c20e923beddde1dd1e0034aa19176d2.tar.gz"; - sha256 = "040xrsgnip6gqljfyy1ad0l7q41h659h5hqbcn96bzhdiakcr4yc"; + url = "https://github.com/NixOS/nixpkgs/archive/4c95508641fe780efe41885366e03339b95d04fb.tar.gz"; + sha256 = "1wjspwhzdb6d1kz4khd9l0fivxdk2nq3qvj93pql235sb7909ygx"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -55,6 +55,7 @@ stdenv.mkDerivation rec { (ps: [ ps.sphinx ps.sphinx_rtd_theme ps.pexpect ps.beautifulsoup4 ps.antlr4-python3-runtime ps.sphinxcontrib-bibtex ])) antlr4 + ocamlPackages.odoc ] ++ optionals doInstallCheck ( # Test-suite dependencies diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 61cf6bc4cc..33feeed45c 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://ftp.inf.tu-dresden.de/software/windows/cygwin32 - -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://ftp.inf.tu-dresden.de/software/windows/cygwin32
+
+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/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 63d5541f48..8620b01b26 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -226,3 +226,10 @@ : "${quickchick_CI_REF:=master}" : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" + +######################################################################## +# quickchick +######################################################################## +: "${plugin_tutorial_CI_REF:=master}" +: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" +: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" diff --git a/dev/ci/ci-plugin-tutorial.sh b/dev/ci/ci-plugin-tutorial.sh new file mode 100755 index 0000000000..6c26a71a21 --- /dev/null +++ b/dev/ci/ci-plugin-tutorial.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download plugin_tutorial + +( cd "${CI_BUILD_DIR}/plugin_tutorial" && \ + pushd tuto0 && make && popd && \ + pushd tuto1 && make && popd && \ + pushd tuto2 && make && popd && \ + pushd tuto3 && make && popd ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8d0f69626e..fcfa591ce1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-24-V01" +# CACHEKEY: "bionic_coq-V2018-09-25-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -32,33 +32,31 @@ ENV NJOBS="2" \ OPAMYES="true" # Base opam is the set of base packages required by Coq -ENV COMPILER="4.02.3" +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.2.1 ounit.2.0.8" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="6.14" \ +ENV CAMLP5_VER="7.01" \ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" -# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3 +# base switch RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ - opam install ocamlfind.1.8.0 && \ opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM # base+32bit switch RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install ocamlfind.1.8.0 && \ opam install $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0" + BASE_OPAM_EDGE="dune-release.0.3.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 31bd65af08..09e9762261 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -1,119 +1,120 @@ -@ECHO OFF - -REM This script builds and signs the Windows packages on Gitlab - -ECHO "Start Time" -TIME /T - -REM List currently used cygwin and target folders for debugging / maintenance purposes - -ECHO "Currently used cygwin folders" -DIR C:\cygwin* -ECHO "Currently used target folders" -DIR C:\coq* - -if %ARCH% == 32 ( - SET ARCHLONG=i686 - SET CYGROOT=C:\cygwin - SET SETUP=setup-x86.exe -) - -if %ARCH% == 64 ( - SET ARCHLONG=x86_64 - SET CYGROOT=C:\cygwin64 - SET SETUP=setup-x86_64.exe -) - -SET DESTCOQ=C:\coq%ARCH%_inst - -CALL :MakeUniqueFolder %CYGROOT% CYGROOT -CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ - -powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')" -SET CYGCACHE=%CYGROOT%\var\cache\setup -SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/% -SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/% -SET COQREGTESTING=Y -SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin - -if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build -if exist %DESTCOQ%\ rd /s /q %DESTCOQ% - -call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ - -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^ - -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ - -addon="bignums ltac2 equations" -make=N ^ - -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit - - -ECHO "Start Artifact Creation" -TIME /T - -mkdir artifacts - -CALL :CopyLogFiles - -copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit -REM The open source archive is only required for release builds -IF DEFINED WIN_CERTIFICATE_PATH ( - 7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit -) ELSE ( - REM In non release builds, create a dummy file - ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt -) - -REM DO NOT echo the signing command below, as this would leak secrets in the logs -IF DEFINED WIN_CERTIFICATE_PATH ( - IF DEFINED WIN_CERTIFICATE_PASSWORD ( - ECHO Signing package - @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe - signtool verify /pa dev\nsis\*.exe - ) -) - -ECHO "Finished Artifact Creation" -TIME /T - -CALL :CleanupFolders - -ECHO "Finished Cleanup" -TIME /T - -GOTO :EOF - -:CopyLogFiles - ECHO Copy log files for artifact upload - MKDIR artifacts\buildlogs - COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs - MKDIR artifacts\filelists - COPY %CYGROOT%\build\filelists\* artifacts\filelists - MKDIR artifacts\flagfiles - COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles - GOTO :EOF - -:CleanupFolders - ECHO "Cleaning %CYGROOT%" - DEL /S /F /Q "%CYGROOT%" > NUL - ECHO "Cleaning %DESTCOQ%" - DEL /S /F /Q "%DESTCOQ%" > NUL - GOTO :EOF - -:MakeUniqueFolder - REM Create a uniquely named folder - REM This script is safe because folder creation is atomic - either we create it or fail - REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this) - REM %2 = name of the variable which receives the unique folder name - SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%" - MKDIR "%UNIQUENAME%" - IF ERRORLEVEL 1 GOTO :MakeUniqueFolder - SET "%2=%UNIQUENAME%" - GOTO :EOF - -:ErrorCopyLogFilesAndExit - CALL :CopyLogFiles - REM fall through - -:ErrorExit - CALL :CleanupFolders - ECHO ERROR %0 failed - EXIT /b 1 +@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+ECHO "Start Time"
+TIME /T
+
+REM List currently used cygwin and target folders for debugging / maintenance purposes
+
+ECHO "Currently used cygwin folders"
+DIR C:\ci\cygwin*
+ECHO "Currently used target folders"
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
+
+if %ARCH% == 32 (
+ SET ARCHLONG=i686
+ SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+ SET ARCHLONG=x86_64
+ SET SETUP=setup-x86_64.exe
+)
+
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
+
+powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
+SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
+SET COQREGTESTING=Y
+SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
+
+if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
+if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+
+call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+ -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
+ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+ -addon="bignums ltac2 equations" -make=N ^
+ -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+mkdir artifacts
+
+CALL :CopyLogFiles
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
+REM The open source archive is only required for release builds
+IF DEFINED WIN_CERTIFICATE_PATH (
+ 7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+) ELSE (
+ REM In non release builds, create a dummy file
+ ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
+)
+
+REM DO NOT echo the signing command below, as this would leak secrets in the logs
+IF DEFINED WIN_CERTIFICATE_PATH (
+ IF DEFINED WIN_CERTIFICATE_PASSWORD (
+ ECHO Signing package
+ @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
+ signtool verify /pa dev\nsis\*.exe
+ )
+)
+
+ECHO "Finished Artifact Creation"
+TIME /T
+
+CALL :CleanupFolders
+
+ECHO "Finished Cleanup"
+TIME /T
+
+GOTO :EOF
+
+:CopyLogFiles
+ ECHO Copy log files for artifact upload
+ MKDIR artifacts\buildlogs
+ COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
+ MKDIR artifacts\filelists
+ COPY %CYGROOT%\build\filelists\* artifacts\filelists
+ MKDIR artifacts\flagfiles
+ COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
+ GOTO :EOF
+
+:CleanupFolders
+ ECHO "Cleaning %CYGROOT%"
+ RMDIR /S /Q "%CYGROOT%"
+ ECHO "Cleaning %DESTCOQ%"
+ RMDIR /S /Q "%DESTCOQ%"
+ GOTO :EOF
+
+:MakeUniqueFolder
+ REM Create a uniquely named folder
+ REM This script is safe because folder creation is atomic - either we create it or fail
+ REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
+ REM %2 = name of the variable which receives the unique folder name
+ SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
+ MKDIR "%UNIQUENAME%"
+ IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
+ SET "%2=%UNIQUENAME%"
+ GOTO :EOF
+
+:ErrorCopyLogFilesAndExit
+ CALL :CopyLogFiles
+ REM fall through
+
+:ErrorExit
+ CALL :CleanupFolders
+ ECHO ERROR %0 failed
+ EXIT /b 1
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 85aaf317ef..7349360be8 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -3,29 +3,45 @@ Dune-based build system. If you want to enhance the build system itself (or are curious about its implementation details), see build-system.dev.txt, and in particular its initial HISTORY section. -Dune -==== +About Dune +========== -Coq can now be built using -[Dune](https://github.com/ocaml/dune). Contrary to other systems, -Dune, doesn't use a global`makefile` but local build files named -`dune` that are later composed to form a global build. +Coq can now be built using [Dune](https://github.com/ocaml/dune). + +## Quick Start + +You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq +libraries. No call to `./configure` is needed. + +Dune will get confused if it finds leftovers of in-tree compilation, +so please be sure your tree is clean from objects files generated by +the make-based system. + +If you want to build the standard libraries and plugins you should +call `make -f Makefile.dune voboot`. It is usually enough to do that +once per-session. + +More helper targets are availabe in `Makefile.dune`, `make -f +Makefile.dune` will display some help. + +Dune places build artifacts in a separate directory `_build`; it will +also generate an `.install` file so files can be properly installed by +package managers. + +Contrary to other systems, Dune doesn't use a global `Makefile` but +local build files named `dune` that are later composed to form a +global build. As a developer, Dune should take care of all OCaml-related build tasks -including library management, merlin files, and link order. You are +including library management, merlin files, and linking order. You are are not supposed to modify the `dune` files unless you are adding a new binary, library, or plugin. -The current Dune setup also doesn't require a call to `configure`. The -auto-generated configuration files are properly included in the -dependency graph so it will be automatically generated by Dune with -reasonable developer defaults. You can still override the defaults by -manually calling `./configure`, but note that some configure options -such as install paths are not used by Dune. +## Per-User Custom Settings -Dune uses a separate directory `_build` to store build artifacts; it -will generate an `.install` file so artifacts in the build can be -properly installed by package managers. +Dune will read the file `~/.config/dune/config`; see `man +dune-config`. Among others, you can set in this file the custom number +of build threads `(jobs N)` and display options `(display _mode_)`. ## Targets @@ -36,8 +52,10 @@ project, creating an "install" overlay in `_build/install/default`. You can build some other target by doing `dune build $TARGET`. In order to build a single package, you can do `dune build -$PACKAGE.install`. Dune also provides targets for documentation and -testing, see below. +$PACKAGE.install`. + +Dune also provides targets for documentation, testing, and release +builds, please see below. ## Developer shell @@ -66,7 +84,8 @@ current Coq source tree contains two packages [Coq and CoqIDE], and in the OPAM CoqIDE package we don't want to build CoqIDE against the local copy of Coq. For this purpose, Dune supports the `-p` option, so `dune build -p coqide` will build CoqIDE against the system-installed -version of Coq libs. +version of Coq libs, and use a "release" profile that for example +enables stronger compiler optimizations. ## Stanzas diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 45766293c7..29e87df6b8 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux. In Coq source folder: -opam switch 4.02.3+fp +opam switch 4.05.0+trunk+fp ./configure -local -debug make perf record -g bin/coqtop -compile file.v diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4ad952bdfb..01240a062c 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -219,6 +219,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo Print nat. Definition a := 1. + The blank line after the directive is required. If you begin a proof, + include an ``Abort`` afterwards to reset coqtop for the next example. + Here is a list of permissible options: - Display options diff --git a/doc/sphinx/_static/diffs-coqide-compacted.png b/doc/sphinx/_static/diffs-coqide-compacted.png Binary files differnew file mode 100644 index 0000000000..b64ffeb269 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-compacted.png diff --git a/doc/sphinx/_static/diffs-coqide-multigoal.png b/doc/sphinx/_static/diffs-coqide-multigoal.png Binary files differnew file mode 100644 index 0000000000..4020279267 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-multigoal.png diff --git a/doc/sphinx/_static/diffs-coqide-on.png b/doc/sphinx/_static/diffs-coqide-on.png Binary files differnew file mode 100644 index 0000000000..f270397ea3 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-on.png diff --git a/doc/sphinx/_static/diffs-coqide-removed.png b/doc/sphinx/_static/diffs-coqide-removed.png Binary files differnew file mode 100644 index 0000000000..8f2e71fdc8 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-removed.png diff --git a/doc/sphinx/_static/diffs-coqtop-compacted.png b/doc/sphinx/_static/diffs-coqtop-compacted.png Binary files differnew file mode 100644 index 0000000000..b37f0a6771 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-compacted.png diff --git a/doc/sphinx/_static/diffs-coqtop-multigoal.png b/doc/sphinx/_static/diffs-coqtop-multigoal.png Binary files differnew file mode 100644 index 0000000000..cfedde02ac --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-multigoal.png diff --git a/doc/sphinx/_static/diffs-coqtop-on.png b/doc/sphinx/_static/diffs-coqtop-on.png Binary files differnew file mode 100644 index 0000000000..bdfcf0af1a --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-on.png diff --git a/doc/sphinx/_static/diffs-coqtop-on3.png b/doc/sphinx/_static/diffs-coqtop-on3.png Binary files differnew file mode 100644 index 0000000000..63ff869432 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-on3.png diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index aa8537c92d..d9eaa2c6c6 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -294,6 +294,17 @@ s}, year = {1994} } +@Article{Myers, + author = {Eugene Myers}, + title = {An {O(ND)} difference algorithm and its variations}, + journal = {Algorithmica}, + volume = {1}, + number = {2}, + year = {1986}, + bibsource = {https://link.springer.com/article/10.1007\%2FBF01840446}, + url = {http://www.xmailserver.org/diff2.pdf} +} + @InProceedings{Parent95b, author = {C. Parent}, booktitle = {{Mathematics of Program Construction'95}}, diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 343ca9ed7d..de9e327740 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -85,6 +85,8 @@ Some |Coq| commands call other |Coq| commands. In this case, they look for the commands in directory specified by ``$COQBIN``. If this variable is not set, they look for the commands in the executable path. +.. _COQ_COLORS: + The ``$COQ_COLORS`` environment variable can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated @@ -93,6 +95,15 @@ list of assignments of the form :n:`name={*; attr}` where ANSI escape code. The list of highlight tags can be retrieved with the ``-list-tags`` command-line option of ``coqtop``. +The string uses ANSI escape codes to represent attributes. For example: + + ``export COQ_COLORS=”diff.added=4;48;2;0;0;240:diff.removed=41”`` + +sets the highlights for added text in diffs to underlined (the 4) with a background RGB +color (0, 0, 240) and for removed text in diffs to a red background. +Note that if you specify ``COQ_COLORS``, the predefined attributes are ignored. + + .. _command-line-options: By command line options @@ -164,9 +175,13 @@ and ``coqtop``, unless stated otherwise: :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section :ref:`controlling-display`). -:-color (on|off|auto): Enable or not the coloring of output of `coqtop`. - Default is auto, meaning that `coqtop` dynamically decides, depending on - whether the output channel supports ANSI escape sequences. +:-color (on|off|auto): *Coqtop only*. Enable or disable color output. + Default is auto, meaning color is shown only if + the output channel supports ANSI escape sequences. +:-diffs (on|off|removed): *Coqtop only*. Controls highlighting of differences + between proof steps. ``on`` highlights added tokens, ``removed`` highlights both added and + removed tokens. Requires that ``–color`` is enabled. (see Section + :ref:`showing_diffs`). :-beautify: Pretty-print each command to *file.beautified* when compiling *file.v*, in order to get old-fashioned syntax/definitions/notations. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 4b1b7719c5..46851050ac 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -495,6 +495,10 @@ Requesting information eexists ?[n]. Show n. + .. coqtop:: none + + Abort. + .. cmdv:: Show Script :name: Show Script @@ -581,6 +585,164 @@ Requesting information fixpoint and cofixpoint is violated at some time of the construction of the proof without having to wait the completion of the proof. +.. _showing_diffs: + +Showing differences between proof steps +--------------------------------------- + + +Coq can automatically highlight the differences between successive proof steps. +For example, the following screenshots of CoqIDE and coqtop show the application +of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. +The conclusion is entirely in pale green because although it’s changed, no tokens were added +to it. The second screenshot uses the "removed" option, so it shows the conclusion a +second time with the old text, with deletions marked in red. Also, since the hypotheses are +new, no line of old text is shown for them. + +.. comment screenshot produced with: + Inductive ev : nat -> Prop := + | ev_0 : ev 0 + | ev_SS : forall n : nat, ev n -> ev (S (S n)). + + Fixpoint double (n:nat) := + match n with + | O => O + | S n' => S (S (double n')) + end. + + Goal forall n, ev n -> exists k, n = double k. + intros n E. + +.. + + .. image:: ../_static/diffs-coqide-on.png + :alt: |CoqIDE| with Set Diffs on + +.. + + .. image:: ../_static/diffs-coqide-removed.png + :alt: |CoqIDE| with Set Diffs removed + +.. + + .. image:: ../_static/diffs-coqtop-on3.png + :alt: coqtop with Set Diffs on + +How to enable diffs +``````````````````` + +.. opt:: Diffs %( "on" %| "off" %| "removed" %) + + .. This ref doesn't work: :opt:`Set Diffs %( "on" %| "off" %| "removed" %)` + + The “on” option highlights added tokens in green, while the “removed” option + additionally reprints items with removed tokens in red. Unchanged tokens in + modified items are shown with pale green or red. (Colors are user-configurable.) + +For coqtop, showing diffs can be enabled when starting coqtop with the +``-diffs on|off|removed`` command-line option or with the ``Set Diffs`` +command within Coq. You will need to provide the ``-color on|auto`` command-line option when +you start coqtop in either case. + +Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment +variable. See section :ref:`customization-by-environment-variables`. Diffs +use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. + +In CoqIDE, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` +command in CoqIDE. You can change the background colors shown for diffs from the +``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, +``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also +lets you control other attributes of the highlights, such as the foreground +color, bold, italic, underline and strikeout. + +Note: As of this writing (August 2018), Proof General will need minor changes +to be able to show diffs correctly. We hope it will support this feature soon. +See https://github.com/ProofGeneral/PG/issues/381 for the current status. + +How diffs are calculated +```````````````````````` + +Diffs are calculated as follows: + +1. Select the old proof state to compare to, which is the proof state before + the last tactic that changed the proof. Changes that only affect the view + of the proof, such as ``all: swap 1 2``, are ignored. + +2. For each goal in the new proof state, determine what old goal to compare + it to—the one it is derived from or is the same as. Match the hypotheses by + name (order is ignored), handling compacted items specially. + +3. For each hypothesis and conclusion (the “items”) in each goal, pass + them as strings to the lexer to break them into tokens. Then apply the + Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting. + +Notes: + +* Aside from the highlights, output for the "on" option should be identical + to the undiffed output. +* Goals completed in the last proof step will not be shown even with the + "removed" setting. + +.. comment The following screenshots show diffs working with multiple goals and with compacted + hypotheses. In the first one, notice that the goal ``P 1`` is not highlighted at + all after the split because it has not changed. + + .. todo: Use this script and remove the screenshots when COQ_COLORS + works for coqtop in sphinx + .. coqtop:: none + + Set Diffs "on". + Parameter P : nat -> Prop. + Goal P 1 /\ P 2 /\ P 3. + + .. coqtop:: out + + split. + + .. coqtop:: all + + 2: split. + + .. coqtop:: none + + Abort. + + .. + + .. coqtop:: none + + Set Diffs "on". + Goal forall n m : nat, n + m = m + n. + Set Diffs "on". + + .. coqtop:: out + + intros n. + + .. coqtop:: all + + intros m. + + .. coqtop:: none + + Abort. + +This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal +with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after +the split because it has not changed. + +.. + + .. image:: ../_static/diffs-coqide-multigoal.png + :alt: coqide with Set Diffs on with multiple goals + +This is how diffs may appear after applying a :tacn:`intro` tactic that results +in compacted hypotheses: + +.. + + .. image:: ../_static/diffs-coqide-compacted.png + :alt: coqide with Set Diffs on with compacted hyptotheses Controlling the effect of proof editing commands ------------------------------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index f99c539251..db9f04ba11 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2214,6 +2214,7 @@ and an explanation of the underlying technique. ``simple inversion``. .. tacv:: inversion @ident using @ident + :name: inversion ... using ... Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 59cad3bea2..eacd7b4676 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -12,13 +12,15 @@ The ``Scheme`` command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema: -.. cmd:: Scheme @ident := Induction for @ident Sort sort {* with @ident := Induction for @ident Sort sort} +.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort sort {* with @ident__i := Induction for @ident__j Sort sort} -where each `ident'ᵢ` is a different inductive type identifier -belonging to the same package of mutual inductive definitions. This -command generates the `identᵢ`s to be mutually recursive -definitions. Each term `identᵢ` proves a general principle of mutual -induction for objects in type `identᵢ`. + This command is a high-level tool for generating automatically + (possibly mutual) induction principles for given types and sorts. + Each :n:`@ident__j` is a different inductive type identifier belonging to + the same package of mutual inductive definitions. + The command generates the :n:`@ident__i`\s to be mutually recursive + definitions. Each term :n:`@ident__i` proves a general principle of mutual + induction for objects in type :n:`@ident__j`. .. cmdv:: Scheme @ident := Minimality for @ident Sort sort {* with @ident := Minimality for @ident' Sort sort} @@ -44,9 +46,9 @@ induction for objects in type `identᵢ`. .. coqtop:: none - Axiom A : Set. - Axiom B : Set. - + Axiom A : Set. + Axiom B : Set. + .. coqtop:: all Inductive tree : Set := node : A -> forest -> tree @@ -79,7 +81,7 @@ induction for objects in type `identᵢ`. .. coqtop:: all Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n) - with even : nat -> Prop := + with even : nat -> Prop := | evenO : even 0 | evenS : forall n:nat, odd n -> even (S n). @@ -136,19 +138,20 @@ Automatic declaration of schemes Combined Scheme ~~~~~~~~~~~~~~~~~~~~~~ -The ``Combined Scheme`` command is a tool for combining induction -principles generated by the ``Scheme command``. Its syntax follows the -schema : - -.. cmd:: Combined Scheme @ident from {+, ident} +.. cmd:: Combined Scheme @ident from {+, @ident__i} -where each identᵢ after the ``from`` is a different inductive principle that must -belong to the same package of mutual inductive principle definitions. -This command generates the leftmost `ident` to be the conjunction of the -principles: it is built from the common premises of the principles and -concluded by the conjunction of their conclusions. + This command is a tool for combining induction principles generated + by the :cmd:`Scheme` command. + Each :n:`@ident__i` is a different inductive principle that must belong + to the same package of mutual inductive principle definitions. + This command generates :n:`@ident` to be the conjunction of the + principles: it is built from the common premises of the principles + and concluded by the conjunction of their conclusions. + In the case where all the inductive principles used are in sort + ``Prop``, the propositional conjunction ``and`` is used, otherwise + the simple product ``prod`` is used instead. -.. example:: +.. example:: We can define the induction principles for trees and forests using: @@ -170,6 +173,23 @@ concluded by the conjunction of their conclusions. Check tree_forest_mutind. +.. example:: + + We can also combine schemes at sort ``Type``: + + .. coqtop:: all + + Scheme tree_forest_rect := Induction for tree Sort Type + with forest_tree_rect := Induction for forest Sort Type. + + .. coqtop:: all + + Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect. + + .. coqtop:: all + + Check tree_forest_mutrect. + .. _functional-scheme: Generation of induction principles with ``Functional`` ``Scheme`` @@ -186,7 +206,7 @@ schema: where each `ident'ᵢ` is a different mutually defined function name (the names must be in the same order as when they were defined). This command generates the induction principle for each `identᵢ`, following -the recursive structure and case analyses of the corresponding function +the recursive structure and case analyses of the corresponding function identᵢ’. .. warning:: @@ -196,7 +216,7 @@ identᵢ’. :cmd:`Function` generally produces smaller principles that are closer to how a user would implement them. See :ref:`advanced-recursive-functions` for details. -.. example:: +.. example:: Induction scheme for div2. @@ -262,11 +282,11 @@ identᵢ’. We define trees by the following mutual inductive type: .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning - + .. coqtop:: reset all Axiom A : Set. - + Inductive tree : Set := node : A -> forest -> tree with forest : Set := @@ -313,20 +333,21 @@ identᵢ’. Check tree_size_ind2. .. _derive-inversion: - + Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -The syntax of ``Derive`` ``Inversion`` follows the schema: - .. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort -This command generates an inversion principle for the `inversion … using` -tactic. Let `I` be an inductive predicate and `x` the variables occurring -in t. This command generates and stocks the inversion lemma for the -sort `sort` corresponding to the instance `∀ (x:T), I t` with the name -`ident` in the global environment. When applied, it is equivalent to -having inverted the instance with the tactic `inversion`. + This command generates an inversion principle for the + :tacn:`inversion ... using ...` tactic. Let :g:`I` be an inductive + predicate and :g:`x` the variables occurring in t. This command + generates and stocks the inversion lemma for the sort :g:`sort` + corresponding to the instance :g:`∀ (x:T), I t` with the name + :n:`@ident` in the global environment. When applied, it is + equivalent to having inverted the instance with the tactic + :g:`inversion`. + .. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort @@ -347,7 +368,7 @@ having inverted the instance with the tactic `inversion`. Consider the relation `Le` over natural numbers and the following parameter ``P``: - + .. coqtop:: all Inductive Le : nat -> nat -> Set := @@ -370,9 +391,9 @@ having inverted the instance with the tactic `inversion`. .. coqtop:: none - Goal forall (n m : nat) (H : Le (S n) m), P n m. + Goal forall (n m : nat) (H : Le (S n) m), P n m. intros. - + .. coqtop:: all Show. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index edf4e6ec9d..2c69dcfe08 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -560,6 +560,9 @@ class CoqtopDirective(Directive): Print nat. Definition a := 1. + The blank line after the directive is required. If you begin a proof, + include an ``Abort`` afterwards to reset coqtop for the next example. + Here is a list of permissible options: - Display options diff --git a/dune-project b/dune-project index 6ce4ec4717..607e5a68a5 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 1.1) +(lang dune 1.2) -(name coq-devel) +(name coq) diff --git a/dune-workspace b/dune-workspace index ee206e8e17..38875eac2c 100644 --- a/dune-workspace +++ b/dune-workspace @@ -1,4 +1,4 @@ -(lang dune 1.1) +(lang dune 1.2) ; Add custom flags here. Default developer profile is `dev` (env diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 678f7c6ce6..8ab3ce821e 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -14,7 +14,23 @@ open Names open Constr open Context -include Evd.MiniEConstr +module ESorts = struct + include Evd.MiniEConstr.ESorts + + let equal sigma s1 s2 = + Sorts.equal (kind sigma s1) (kind sigma s2) +end + +module EInstance = struct + include Evd.MiniEConstr.EInstance + + let equal sigma i1 i2 = + Univ.Instance.equal (kind sigma i1) (kind sigma i2) +end + +include (Evd.MiniEConstr : module type of Evd.MiniEConstr + with module ESorts := ESorts + and module EInstance := EInstance) type types = t type constr = t @@ -445,38 +461,28 @@ let fold sigma f acc c = match kind sigma c with let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2 -let eq_einstance sigma i1 i2 = - let i1 = EInstance.kind sigma (EInstance.make i1) in - let i2 = EInstance.kind sigma (EInstance.make i2) in - Univ.Instance.equal i1 i2 - -let eq_esorts sigma s1 s2 = - let s1 = ESorts.kind sigma (ESorts.make s1) in - let s2 = ESorts.kind sigma (ESorts.make s2) in - Sorts.equal s1 s2 - let eq_constr sigma c1 c2 = - let kind c = kind_upto sigma c in - let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in - let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in + let kind c = kind sigma c in + let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in + let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in let rec eq_constr nargs c1 c2 = compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2 in - eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) + eq_constr 0 c1 c2 let eq_constr_nounivs sigma c1 c2 = - let kind c = kind_upto sigma c in + let kind c = kind sigma c in let rec eq_constr nargs c1 c2 = compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2 in - eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) + eq_constr 0 c1 c2 let compare_constr sigma cmp c1 c2 = - let kind c = kind_upto sigma c in - let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in - let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in - let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in - compare_gen kind eq_inst eq_sorts cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) + let kind c = kind sigma c in + let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in + let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in + let cmp nargs c1 c2 = cmp c1 c2 in + compare_gen kind eq_inst eq_sorts cmp 0 c1 c2 let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = let open UnivProblem in @@ -528,10 +534,10 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2) let eq_universes env sigma cstrs cv_pb ref nargs l l' = - if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true) + if EInstance.is_empty l then (assert (EInstance.is_empty l'); true) else - let l = Evd.normalize_universe_instance sigma l - and l' = Evd.normalize_universe_instance sigma l' in + let l = EInstance.kind sigma l + and l' = EInstance.kind sigma l' in let open GlobRef in let open UnivProblem in match ref with @@ -549,7 +555,7 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' = let test_constr_universes env sigma leq m n = let open UnivProblem in - let kind c = kind_upto sigma c in + let kind c = kind sigma c in if m == n then Some Set.empty else let cstrs = ref Set.empty in @@ -557,16 +563,16 @@ let test_constr_universes env sigma leq m n = let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l' and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in let eq_sorts s1 s2 = - let s1 = ESorts.kind sigma (ESorts.make s1) in - let s2 = ESorts.kind sigma (ESorts.make s2) in + let s1 = ESorts.kind sigma s1 in + let s2 = ESorts.kind sigma s2 in if Sorts.equal s1 s2 then true else (cstrs := Set.add (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in let leq_sorts s1 s2 = - let s1 = ESorts.kind sigma (ESorts.make s1) in - let s2 = ESorts.kind sigma (ESorts.make s2) in + let s1 = ESorts.kind sigma s1 in + let s2 = ESorts.kind sigma s2 in if Sorts.equal s1 s2 then true else (cstrs := Set.add @@ -587,16 +593,16 @@ let test_constr_universes env sigma leq m n = if res then Some !cstrs else None let eq_constr_universes env sigma m n = - test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n) + test_constr_universes env sigma false m n let leq_constr_universes env sigma m n = - test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n) + test_constr_universes env sigma true m n let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = - let kind c = kind_upto sigma c in - match kind_upto sigma m, kind_upto sigma n with + let kind c = kind sigma c in + match kind m, kind n with | Proj (p, c), App (f, args) | App (f, args), Proj (p, c) -> - (match kind_upto sigma f with + (match kind f with | Const (p', u) when Constant.equal (Projection.constant p) p' -> let npars = Projection.npars p in if Array.length args == npars + 1 then @@ -612,6 +618,8 @@ let eq_constr_universes_proj env sigma m n = let cstrs = ref Set.empty in let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in let eq_sorts s1 s2 = + let s1 = ESorts.kind sigma s1 in + let s2 = ESorts.kind sigma s2 in if Sorts.equal s1 s2 then true else (cstrs := Set.add @@ -621,7 +629,7 @@ let eq_constr_universes_proj env sigma m n = let rec eq_constr' nargs m n = m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n in - let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in + let res = eq_constr' 0 m n in if res then Some !cstrs else None let universes_of_constr sigma c = diff --git a/kernel/.merlin.in b/kernel/.merlin.in new file mode 100644 index 0000000000..912ff61496 --- /dev/null +++ b/kernel/.merlin.in @@ -0,0 +1,8 @@ +FLG -rectypes -thread -safe-string -w +a-4-44-50 + +S ../clib +B ../clib +S ../config +B ../config +S ../lib +B ../lib diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c4c96c9b55..003b49535f 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -551,45 +551,7 @@ let mk_clos_vect env v = match v with [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] | v -> Array.Fun1.map mk_clos env v -(* Translate the head constructor of t from constr to fconstr. This - function is parameterized by the function to apply on the direct - subterms. - Could be used insted of mk_clos. *) -let mk_clos_deep clos_fun env t = - match kind t with - | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> - mk_clos env t - | Cast (a,k,b) -> - { norm = Red; - term = FCast (clos_fun env a, k, clos_fun env b)} - | App (f,v) -> - { norm = Red; - term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) } - | Proj (p,c) -> - { norm = Red; - term = FProj (p, clos_fun env c) } - | Case (ci,p,c,v) -> - { norm = Red; - term = FCaseT (ci, p, clos_fun env c, v, env) } - | Fix fx -> - { norm = Cstr; term = FFix (fx, env) } - | CoFix cfx -> - { norm = Cstr; term = FCoFix(cfx,env) } - | Lambda _ -> - { norm = Cstr; term = mk_lambda env t } - | Prod (n,t,c) -> - { norm = Whnf; - term = FProd (n, clos_fun env t, clos_fun (subs_lift env) c) } - | LetIn (n,b,t,c) -> - { norm = Red; - term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } - | Evar ev -> - { norm = Red; term = FEvar(ev,env) } - -(* A better mk_clos? *) -let mk_clos2 = mk_clos_deep mk_clos - -(* The inverse of mk_clos_deep: move back to constr *) +(* The inverse of mk_clos: move back to constr *) let rec to_constr lfts v = match v.term with | FRel i -> mkRel (reloc_rel i lfts) @@ -922,13 +884,18 @@ and knht info e t stk = knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk) - | Fix _ -> knh info (mk_clos2 e t) stk + | Fix fx -> knh info { norm = Cstr; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk - | Proj (_p,_c) -> knh info (mk_clos2 e t) stk - | (Lambda _|Prod _|Construct _|CoFix _|Ind _| - LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> - (mk_clos2 e t, stk) + | Proj (p, c) -> knh info { norm = Red; term = FProj (p, mk_clos e c) } stk + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> (mk_clos e t, stk) + | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk + | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk + | Prod (n, t, c) -> + { norm = Whnf; term = FProd (n, mk_clos e t, mk_clos (subs_lift e) c) }, stk + | LetIn (n,b,t,c) -> + { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk + | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk (************************************************************************) diff --git a/kernel/constr.ml b/kernel/constr.ml index b25f38d630..c97969c0e0 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -237,6 +237,17 @@ let mkVar id = Var id let kind c = c +let rec kind_nocast_gen kind c = + match kind c with + | Cast (c, _, _) -> kind_nocast_gen kind c + | App (h, outer) as k -> + (match kind_nocast_gen kind h with + | App (h, inner) -> App (h, Array.append inner outer) + | _ -> k) + | k -> k + +let kind_nocast c = kind_nocast_gen kind c + (* The other way around. We treat specifically smart constructors *) let of_kind = function | App (f, a) -> mkApp (f, a) @@ -755,10 +766,10 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) -type instance_compare_fn = GlobRef.t -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool -type constr_compare_fn = int -> constr -> constr -> bool +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and [c2] (using [k1] to expose the structure of [c1] and [k2] to expose @@ -772,19 +783,16 @@ type constr_compare_fn = int -> constr -> constr -> bool calls to {!Array.equal_norefl}). *) let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = - match kind1 t1, kind2 t2 with + match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with + | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Sort s1, Sort s2 -> leq_sorts s1 s2 - | Cast (c1, _, _), _ -> leq nargs c1 t2 - | _, Cast (c2, _, _) -> leq nargs t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 (* Why do we suddenly make a special case for Cast here? *) - | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2 - | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2)) | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && diff --git a/kernel/constr.mli b/kernel/constr.mli index ea38dabd5c..2efdae007c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -241,6 +241,11 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr +val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) + +val kind_nocast : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term + (** {6 Simple case analysis} *) val isRel : constr -> bool val isRelN : int -> constr -> bool @@ -518,50 +523,50 @@ val iter_with_binders : val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -type constr_compare_fn = int -> constr -> constr -> bool +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head : constr_compare_fn -> constr_compare_fn +val compare_head : constr constr_compare_fn -> constr constr_compare_fn (** Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .*) -type instance_compare_fn = GlobRef.t -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to compare universe instances, [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen : instance_compare_fn -> +val compare_head_gen : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn val compare_head_gen_leq_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) is used,rather than {!kind}, to expose the immediate subterms of [c1] (resp. [c2]). *) val compare_head_gen_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for @@ -570,11 +575,11 @@ val compare_head_gen_with : [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen_leq : instance_compare_fn -> +val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn -> + constr constr_compare_fn (** {6 Hashconsing} *) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index f0473a5170..d294f2060e 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -88,16 +88,7 @@ let call_compiler ?profile:(profile=false) ml_filename = else [] in - let flambda_args = - if Coq_config.caml_version_nums >= [4;3;0] && Dynlink.is_native then - (* We play safe for now, and use the native compiler - with -Oclassic, however it is likely that `native_compute` - users can benefit from tweaking here. - *) - ["-Oclassic"] - else - [] - in + let flambda_args = if Sys.(backend_type = Native) then ["-Oclassic"] else [] in let args = initial_args @ profile_args @ diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9d302c69fb..b036aa6a67 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -273,7 +273,6 @@ let add_constraints_list cst senv = List.fold_left (fun acc c -> add_constraints c acc) senv cst let push_context_set poly ctx = add_constraints (Now (poly,ctx)) -let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx)) let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 08b97b718e..6e0febaa3f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -128,9 +128,6 @@ val add_modtype : val push_context_set : bool -> Univ.ContextSet.t -> safe_transformer0 -val push_context : - bool -> Univ.UContext.t -> safe_transformer0 - val add_constraints : Univ.Constraint.t -> safe_transformer0 diff --git a/library/coqlib.ml b/library/coqlib.ml index 36a9598f36..026b7aa316 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -349,6 +349,9 @@ let coq_iff = lazy_init_reference ["Logic"] "iff" let coq_iff_left_proj = lazy_init_reference ["Logic"] "proj1" let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2" +let coq_prod = lazy_init_reference ["Datatypes"] "prod" +let coq_pair = lazy_init_reference ["Datatypes"] "pair" + (* Runtime part *) let build_coq_True () = Lazy.force coq_True let build_coq_I () = Lazy.force coq_I @@ -364,6 +367,9 @@ let build_coq_iff () = Lazy.force coq_iff let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj +let build_coq_prod () = Lazy.force coq_prod +let build_coq_pair () = Lazy.force coq_pair + (* The following is less readable but does not depend on parsing *) let coq_eq_ref = lazy (init_reference ["Logic"] "eq") diff --git a/library/coqlib.mli b/library/coqlib.mli index b4bd1b0e06..8844684957 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -101,7 +101,7 @@ val glob_jmeq : GlobRef.t at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the [constr delayed] and [constr_pattern delayed] types. Objects of this time needs to be - forced with [delayed_force] to get the actual constr or pattern + forced with [delayed_force] to get the actual constr or pattern at runtime. *) type coq_bool_data = { @@ -167,7 +167,7 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed val build_coq_sumbool : GlobRef.t delayed (** {6 ... } *) -(** Connectives +(** Connectives The False proposition *) val build_coq_False : GlobRef.t delayed @@ -186,6 +186,10 @@ val build_coq_iff : GlobRef.t delayed val build_coq_iff_left_proj : GlobRef.t delayed val build_coq_iff_right_proj : GlobRef.t delayed +(** Pairs *) +val build_coq_prod : GlobRef.t delayed +val build_coq_pair : GlobRef.t delayed + (** Disjunction *) val build_coq_or : GlobRef.t delayed diff --git a/library/global.ml b/library/global.ml index 5872126a12..e872d081d6 100644 --- a/library/global.ml +++ b/library/global.ml @@ -86,7 +86,6 @@ let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) -let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) diff --git a/library/global.mli b/library/global.mli index 6aeae9fd02..5205968c7b 100644 --- a/library/global.mli +++ b/library/global.mli @@ -49,7 +49,6 @@ val add_mind : (** Extra universe constraints *) val add_constraints : Univ.Constraint.t -> unit -val push_context : bool -> Univ.UContext.t -> unit val push_context_set : bool -> Univ.ContextSet.t -> unit (** Non-interactive modules and module types *) diff --git a/printing/printer.ml b/printing/printer.ml index 6cd4daa374..cfa3e8b6e9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -87,7 +87,6 @@ let pr_leconstr_core = Proof_diffs.pr_leconstr_core let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c) let pr_lconstr_env = Proof_diffs.pr_lconstr_env let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c) -let _ = Hook.set Refine.pr_constr pr_constr_env let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c) let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c) diff --git a/proofs/refine.ml b/proofs/refine.ml index 198e057ebc..05474d5f84 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -44,9 +44,6 @@ let typecheck_evar ev env sigma = let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in sigma -let (pr_constrv,pr_constr) = - Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () - (* Get the side-effect's constant declarations to update the monad's * environmnent *) let add_if_undefined env eff = @@ -111,7 +108,7 @@ let generic_refine ~typecheck f gl = let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ - Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in + Termops.Internal.print_constr_env env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> diff --git a/proofs/refine.mli b/proofs/refine.mli index 70a23a9fba..1af6463a02 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -17,10 +17,6 @@ open Proofview (** {6 The refine tactic} *) -(** Printer used to print the constr which refine refines. *) -val pr_constr : - (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t - (** {7 Refinement primitives} *) val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 182b38d350..9e42a71ea8 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -227,4 +227,9 @@ module New = struct let pf_nf_evar gl t = nf_evar (project gl) t + let pf_undefined_evars gl = + let sigma = Proofview.Goal.sigma gl in + let ev = Proofview.Goal.goal gl in + let evi = Evd.find sigma ev in + Evarutil.filtered_undefined_evars_of_evar_info sigma evi end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 31496fb3d5..b4cb2be2b8 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -95,7 +95,7 @@ val refine : constr -> tactic val pr_gls : goal sigma -> Pp.t val pr_glls : goal list sigma -> Pp.t -(* Variants of [Tacmach] functions built with the new proof engine *) +(** Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t @@ -139,4 +139,6 @@ module New : sig val pf_nf_evar : Proofview.Goal.t -> constr -> constr + (** Gathers the undefined evars of the given goal. *) + val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t end @@ -1,4 +1,3 @@ -# Some developers don't want a pinned nix-shell by default. -# If you want to use the pin nix-shell or a more sophisticated set of arguments: +# If you want to use a more sophisticated set of arguments: # $ nix-shell default.nix --arg shell true -import ./default.nix { pkgs = import <nixpkgs> {}; shell = true; } +import ./default.nix { shell = true; } diff --git a/tactics/auto.ml b/tactics/auto.ml index d7de6c4fb5..65b2615b6b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -416,6 +416,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = "nocore" amongst the databases. *) let trivial ?(debug=Off) lems dbnames = + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -427,6 +428,7 @@ let trivial ?(debug=Off) lems dbnames = end let full_trivial ?(debug=Off) lems = + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -501,6 +503,7 @@ let search d n mod_delta db_list local_db = let default_search_depth = ref 5 let delta_auto debug mod_delta n lems dbnames = + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -524,6 +527,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n let default_auto = auto !default_search_depth [] [] let delta_full_auto ?(debug=Off) mod_delta n lems = + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f3581f17dd..9bd406e14d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -935,6 +935,9 @@ module Search = struct | Some i -> str ", with depth limit " ++ int i)); tac + let eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints = + Hints.wrap_hint_warning @@ eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints + let run_on_evars env evm p tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) @@ -1144,15 +1147,19 @@ let resolve_typeclass_evars debug depth unique env evd filter split fail = (initial_select_evars filter) evd split fail let solve_inst env evd filter unique split fail = - resolve_typeclass_evars + let ((), sigma) = Hints.wrap_hint_warning_fun env evd begin fun evd -> + (), resolve_typeclass_evars (get_typeclasses_debug ()) (get_typeclasses_depth ()) unique env evd filter split fail + end in + sigma let _ = Hook.set Typeclasses.solve_all_instances_hook solve_inst let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = + let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma -> let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl Store.empty in @@ -1170,7 +1177,9 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = let evd = sig_sig gls' in let t' = mkEvar (ev, Array.of_list subst) in let term = Evarutil.nf_evar evd t' in - evd, term + term, evd + end in + (sigma, term) let _ = Hook.set Typeclasses.solve_one_instance_hook @@ -1206,6 +1215,7 @@ let is_ground c = let autoapply c i = let open Proofview.Notations in + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let hintdb = try Hints.searchtable_map i with Not_found -> CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ ".")) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 80d07c5c03..5067315d08 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -409,7 +409,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl = (* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) let eauto_with_bases ?(debug=Off) np lems db_list = - tclTRY (e_search_auto debug np lems db_list) + Proofview.V82.of_tactic (Hints.wrap_hint_warning (Proofview.V82.tactic (tclTRY (e_search_auto debug np lems db_list)))) let eauto ?(debug=Off) np lems dbnames = let db_list = make_db_list dbnames in @@ -420,8 +420,8 @@ let full_eauto ?(debug=Off) n lems gl = tclTRY (e_search_auto debug n lems db_list) gl let gen_eauto ?(debug=Off) np lems = function - | None -> Proofview.V82.tactic (full_eauto ~debug np lems) - | Some l -> Proofview.V82.tactic (eauto ~debug np lems l) + | None -> Hints.wrap_hint_warning (Proofview.V82.tactic (full_eauto ~debug np lems)) + | Some l -> Hints.wrap_hint_warning (Proofview.V82.tactic (eauto ~debug np lems l)) let make_depth = function | None -> !default_search_depth diff --git a/tactics/hints.ml b/tactics/hints.ml index 3835dee299..c0ba363360 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1579,25 +1579,76 @@ let print_mp mp = let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true +let hint_trace = Evd.Store.field () + +let log_hint h = + let open Proofview.Notations in + Proofview.tclEVARMAP >>= fun sigma -> + let store = get_extra_data sigma in + match Store.get store hint_trace with + | None -> + (** All calls to hint logging should be well-scoped *) + assert false + | Some trace -> + let trace = KNmap.add h.uid h trace in + let store = Store.set store hint_trace trace in + Proofview.Unsafe.tclEVARS (set_extra_data store sigma) + let warn_non_imported_hint = CWarnings.create ~name:"non-imported-hint" ~category:"automation" (fun (hint,mp) -> strbrk "Hint used but not imported: " ++ hint ++ print_mp mp) -let warn h x = - let open Proofview in - tclBIND tclENV (fun env -> - tclBIND tclEVARMAP (fun sigma -> - let hint = pr_hint env sigma h in - let (mp, _, _) = KerName.repr h.uid in - warn_non_imported_hint (hint,mp); - Proofview.tclUNIT x)) +let warn env sigma h = + let hint = pr_hint env sigma h in + let (mp, _, _) = KerName.repr h.uid in + warn_non_imported_hint (hint,mp) + +let wrap_hint_warning t = + let open Proofview.Notations in + Proofview.tclEVARMAP >>= fun sigma -> + let store = get_extra_data sigma in + let old = Store.get store hint_trace in + let store = Store.set store hint_trace KNmap.empty in + Proofview.Unsafe.tclEVARS (set_extra_data store sigma) >>= fun () -> + t >>= fun ans -> + Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> + let store = get_extra_data sigma in + let hints = match Store.get store hint_trace with + | None -> assert false + | Some hints -> hints + in + let () = KNmap.iter (fun _ h -> warn env sigma h) hints in + let store = match old with + | None -> Store.remove store hint_trace + | Some v -> Store.set store hint_trace v + in + Proofview.Unsafe.tclEVARS (set_extra_data store sigma) >>= fun () -> + Proofview.tclUNIT ans + +let wrap_hint_warning_fun env sigma t = + let store = get_extra_data sigma in + let old = Store.get store hint_trace in + let store = Store.set store hint_trace KNmap.empty in + let (ans, sigma) = t (set_extra_data store sigma) in + let store = get_extra_data sigma in + let hints = match Store.get store hint_trace with + | None -> assert false + | Some hints -> hints + in + let () = KNmap.iter (fun _ h -> warn env sigma h) hints in + let store = match old with + | None -> Store.remove store hint_trace + | Some v -> Store.set store hint_trace v + in + (ans, set_extra_data store sigma) let run_hint tac k = match !warn_hint with | `LAX -> k tac.obj | `WARN -> if is_imported tac then k tac.obj - else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x) + else Proofview.tclTHEN (log_hint tac) (k tac.obj) | `STRICT -> if is_imported tac then k tac.obj else Proofview.tclZERO (UserError (None, (str "Tactic failure."))) diff --git a/tactics/hints.mli b/tactics/hints.mli index c49ca2094a..d63efea27d 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -282,6 +282,15 @@ val make_db_list : hint_db_name list -> hint_db list val typeclasses_db : hint_db_name val rewrite_db : hint_db_name +val wrap_hint_warning : 'a Proofview.tactic -> 'a Proofview.tactic +(** Use around toplevel calls to hint-using tactics, to enable the tracking of + non-imported hints. Any tactic calling [run_hint] must be wrapped this + way. *) + +val wrap_hint_warning_fun : env -> evar_map -> + (evar_map -> 'a * evar_map) -> 'a * evar_map +(** Variant of the above for non-tactics *) + (** Printing hints *) val pr_searchtable : env -> evar_map -> Pp.t diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index 034684054d..c3f6bebcbe 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -27,41 +27,35 @@ End ListLower. Lemma LowerL_Lem@{i j|j<i+} (A : Type@{j}) (l : List@{i} A) : l = LowerL@{j i} l. Proof. reflexivity. Qed. -(* -I disable these tests because cqochk can't process them when compiled with - ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis! - I have added this file (including the commented parts below) in - test-suite/success/cumulativity.v which doesn't run coqchk on them. -*) -(* Inductive Tp := tp : Type -> Tp. *) +Inductive Tp := tp : Type -> Tp. -(* Section TpLift. *) -(* Universe i j. *) +Section TpLift. -(* Constraint i < j. *) + Universe i j. -(* Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *) + Constraint i < j. -(* End TpLift. *) + Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. -(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *) -(* Proof. reflexivity. Qed. *) +End TpLift. -(* Section TpLower. *) -(* Universe i j. *) +Lemma LiftC_Lem (t : Tp) : LiftTp t = t. +Proof. reflexivity. Qed. -(* Constraint i < j. *) +Section TpLower. + Universe i j. -(* Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *) + Constraint i < j. -(* End TpLower. *) + Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. +End TpLower. -(* Section subtyping_test. *) -(* Universe i j. *) -(* Constraint i < j. *) +Section subtyping_test. + Universe i j. + Constraint i < j. -(* Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *) + Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. -(* End subtyping_test. *) +End subtyping_test. diff --git a/test-suite/success/CombinedScheme.v b/test-suite/success/CombinedScheme.v new file mode 100644 index 0000000000..d6ca7a299f --- /dev/null +++ b/test-suite/success/CombinedScheme.v @@ -0,0 +1,35 @@ +Inductive even (x : bool) : nat -> Type := +| evenO : even x 0 +| evenS : forall n, odd x n -> even x (S n) +with odd (x : bool) : nat -> Type := +| oddS : forall n, even x n -> odd x (S n). + +Scheme even_ind_prop := Induction for even Sort Prop +with odd_ind_prop := Induction for odd Sort Prop. + +Combined Scheme even_cprop from even_ind_prop, odd_ind_prop. + +Check even_cprop : + forall (x : bool) (P : forall n : nat, even x n -> Prop) + (P0 : forall n : nat, odd x n -> Prop), + P 0 (evenO x) -> + (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) -> + (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) -> + (forall (n : nat) (e : even x n), P n e) /\ + (forall (n : nat) (o : odd x n), P0 n o). + +Scheme even_ind_type := Induction for even Sort Type +with odd_ind_type := Induction for odd Sort Type. + +(* This didn't work in v8.7 *) + +Combined Scheme even_ctype from even_ind_type, odd_ind_type. + +Check even_ctype : + forall (x : bool) (P : forall n : nat, even x n -> Prop) + (P0 : forall n : nat, odd x n -> Prop), + P 0 (evenO x) -> + (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) -> + (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) -> + (forall (n : nat) (e : even x n), P n e) * + (forall (n : nat) (o : odd x n), P0 n o). diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 76c39f275d..8a0265438a 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -177,11 +177,12 @@ Arguments inr {A B} _ , A [B] _. the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) Inductive prod (A B:Type) : Type := - pair : A -> B -> prod A B. + pair : A -> B -> A * B + +where "x * y" := (prod x y) : type_scope. Add Printing Let prod. -Notation "x * y" := (prod x y) : type_scope. Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. Arguments pair {A B} _ _. @@ -189,18 +190,14 @@ Arguments pair {A B} _ _. Section projections. Context {A : Type} {B : Type}. - Definition fst (p:A * B) := match p with - | (x, y) => x - end. - Definition snd (p:A * B) := match p with - | (x, y) => y - end. + Definition fst (p:A * B) := match p with (x, y) => x end. + Definition snd (p:A * B) := match p with (x, y) => y end. End projections. Hint Resolve pair inl inr: core. Lemma surjective_pairing : - forall (A B:Type) (p:A * B), p = pair (fst p) (snd p). + forall (A B:Type) (p:A * B), p = (fst p, snd p). Proof. destruct p; reflexivity. Qed. @@ -213,13 +210,19 @@ Proof. rewrite Hfst; rewrite Hsnd; reflexivity. Qed. -Definition prod_uncurry (A B C:Type) (f:prod A B -> C) - (x:A) (y:B) : C := f (pair x y). +Definition prod_uncurry (A B C:Type) (f:A * B -> C) + (x:A) (y:B) : C := f (x,y). Definition prod_curry (A B C:Type) (f:A -> B -> C) - (p:prod A B) : C := match p with - | pair x y => f x y - end. + (p:A * B) : C := match p with (x, y) => f x y end. + +Import EqNotations. + +Lemma rew_pair : forall A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2), + (rew H in y1, rew H in y2) = rew [fun x => (P x * Q x)%type] H in (y1,y2). +Proof. + destruct H. reflexivity. +Defined. (** Polymorphic lists and some operations *) @@ -254,7 +257,6 @@ Definition app (A : Type) : list A -> list A -> list A := | a :: l1 => a :: app l1 m end. - Infix "++" := app (right associativity, at level 60) : list_scope. (* Unset Universe Polymorphism. *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9d60cf54c3..4ec0049a9c 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -406,6 +406,37 @@ End EqNotations. Import EqNotations. +Section equality_dep. + Variable A : Type. + Variable B : A -> Type. + Variable f : forall x, B x. + Variables x y : A. + + Theorem f_equal_dep : forall (H: x = y), rew H in f x = f y. + Proof. + destruct H; reflexivity. + Defined. + +End equality_dep. + +Section equality_dep2. + + Variable A A' : Type. + Variable B : A -> Type. + Variable B' : A' -> Type. + Variable f : A -> A'. + Variable g : forall a:A, B a -> B' (f a). + Variables x y : A. + + Lemma f_equal_dep2 : forall {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a)) + {x1 x2 : A} {y1 : B x1} {y2 : B x2} (H : x1 = x2), + rew H in y1 = y2 -> rew f_equal f H in g x1 y1 = g x2 y2. + Proof. + destruct H, 1. reflexivity. + Defined. + +End equality_dep2. + Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a. Proof. intros. @@ -492,6 +523,42 @@ Proof. destruct e''; reflexivity. Defined. +Theorem rew_map : forall A B (P:B->Type) (f:A->B) x1 x2 (H:x1=x2) (y:P (f x1)), + rew [fun x => P (f x)] H in y = rew f_equal f H in y. +Proof. + destruct H; reflexivity. +Defined. + +Theorem eq_trans_map : forall {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3}, + forall (H1:x1=x2) (H2:x2=x3) (H1': rew H1 in y1 = y2) (H2': rew H2 in y2 = y3), + rew eq_trans H1 H2 in y1 = y3. +Proof. + intros. destruct H2. exact (eq_trans H1' H2'). +Defined. + +Lemma map_subst : forall {A} {P Q:A->Type} (f : forall x, P x -> Q x) {x y} (H:x=y) (z:P x), + rew H in f x z = f y (rew H in z). +Proof. + destruct H. reflexivity. +Defined. + +Lemma map_subst_map : forall {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x)), + forall {x y} (H:x=y) (z:P x), rew f_equal f H in g x z = g y (rew H in z). +Proof. + destruct H. reflexivity. +Defined. + +Lemma rew_swap : forall A (P:A->Type) x1 x2 (H:x1=x2) (y1:P x1) (y2:P x2), rew H in y1 = y2 -> y1 = rew <- H in y2. +Proof. + destruct H. trivial. +Defined. + +Lemma rew_compose : forall A (P:A->Type) x1 x2 x3 (H1:x1=x2) (H2:x2=x3) (y:P x1), + rew H2 in rew H1 in y = rew (eq_trans H1 H2) in y. +Proof. + destruct H2. reflexivity. +Defined. + (** Extra properties of equality *) Theorem eq_id_comm_l : forall A (f:A->A) (Hf:forall a, a = f a), forall a, f_equal f (Hf a) = Hf (f a). diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index db8857df64..d6a0fb214f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -154,6 +154,10 @@ Section Projections. End Projections. +Local Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ; '/ ' y )"). +Local Notation "x .1" := (projT1 x) (at level 1, left associativity, format "x .1"). +Local Notation "x .2" := (projT2 x) (at level 1, left associativity, format "x .2"). + (** [sigT2] of a predicate can be projected to a [sigT]. This allows [projT1] and [projT2] to be usable with [sigT2]. @@ -231,6 +235,7 @@ Proof. Qed. (** Equality of sigma types *) + Import EqNotations. Local Notation "'rew' 'dependent' H 'in' H'" := (match H with @@ -244,18 +249,18 @@ Section sigT. Local Unset Implicit Arguments. (** Projecting an equality of a pair to equality of the first components *) Definition projT1_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v) - : projT1 u = projT1 v - := f_equal (@projT1 _ _) p. + : u.1 = v.1 + := f_equal (fun x => x.1) p. (** Projecting an equality of a pair to equality of the second components *) Definition projT2_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v) - : rew projT1_eq p in projT2 u = projT2 v + : rew projT1_eq p in u.2 = v.2 := rew dependent p in eq_refl. (** Equality of [sigT] is itself a [sigT] (forwards-reasoning version) *) Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (pq : { p : u1 = v1 & rew p in u2 = v2 }) - : existT _ u1 u2 = existT _ v1 v2. + : (u1; u2) = (v1; v2). Proof. destruct pq as [p q]. destruct q; simpl in *. @@ -264,23 +269,55 @@ Section sigT. (** Equality of [sigT] is itself a [sigT] (backwards-reasoning version) *) Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a }) - (pq : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }) + (pq : { p : u.1 = v.1 & rew p in u.2 = v.2 }) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. apply eq_existT_uncurried; exact pq. Defined. + Lemma eq_existT_curried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} + (p : u1 = v1) (q : rew p in u2 = v2) : (u1; u2) = (v1; v2). + Proof. + destruct p, q. reflexivity. + Defined. + + Local Notation "(= u ; v )" := (eq_existT_curried u v) (at level 0, format "(= u ; '/ ' v )"). + + Lemma eq_existT_curried_map {A A' P P'} (f:A -> A') (g:forall u:A, P u -> P' (f u)) + {u1 v1 : A} {u2 : P u1} {v2 : P v1} (p : u1 = v1) (q : rew p in u2 = v2) : + f_equal (fun x => (f x.1; g x.1 x.2)) (= p; q) = + (= f_equal f p; f_equal_dep2 f g p q). + Proof. + destruct p, q. reflexivity. + Defined. + + Lemma eq_existT_curried_trans {A P} {u1 v1 w1 : A} {u2 : P u1} {v2 : P v1} {w2 : P w1} + (p : u1 = v1) (q : rew p in u2 = v2) + (p' : v1 = w1) (q': rew p' in v2 = w2) : + eq_trans (= p; q) (= p'; q') = + (= eq_trans p p'; eq_trans_map p p' q q'). + Proof. + destruct p', q'. reflexivity. + Defined. + + Theorem eq_existT_curried_congr {A P} {u1 v1 : A} {u2 : P u1} {v2 : P v1} + {p p' : u1 = v1} {q : rew p in u2 = v2} {q': rew p' in u2 = v2} + (r : p = p') : rew [fun H => rew H in u2 = v2] r in q = q' -> (= p; q) = (= p'; q'). + Proof. + destruct r, 1. reflexivity. + Qed. + (** Curried version of proving equality of sigma types *) Definition eq_sigT {A : Type} {P : A -> Type} (u v : { a : A & P a }) - (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v) + (p : u.1 = v.1) (q : rew p in u.2 = v.2) : u = v := eq_sigT_uncurried u v (existT _ p q). (** Equality of [sigT] when the property is an hProp *) Definition eq_sigT_hprop {A P} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A & P a }) - (p : projT1 u = projT1 v) + (p : u.1 = v.1) : u = v := eq_sigT u v p (P_hprop _ _ _). @@ -289,7 +326,7 @@ Section sigT. but for simplicity, we don't. *) Definition eq_sigT_uncurried_iff {A P} (u v : { a : A & P a }) - : u = v <-> { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }. + : u = v <-> { p : u.1 = v.1 & rew p in u.2 = v.2 }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ]. Defined. @@ -305,12 +342,12 @@ Section sigT. (** Equivalence of equality of [sigT] involving hProps with equality of the first components *) Definition eq_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A & P a }) - : u = v <-> (projT1 u = projT1 v) + : u = v <-> (u.1 = v.1) := conj (fun p => f_equal (@projT1 _ _) p) (eq_sigT_hprop P_hprop u v). (** Non-dependent classification of equality of [sigT] *) Definition eq_sigT_nondep {A B : Type} (u v : { a : A & B }) - (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) + (p : u.1 = v.1) (q : u.2 = v.2) : u = v := @eq_sigT _ _ u v p (eq_trans (rew_const _ _) q). @@ -319,8 +356,8 @@ Section sigT. : rew [fun a => { p : P a & Q a p }] H in u = existT (Q y) - (rew H in projT1 u) - (rew dependent H in (projT2 u)). + (rew H in u.1) + (rew dependent H in (u.2)). Proof. destruct H, u; reflexivity. Defined. @@ -416,12 +453,12 @@ Section sigT2. : u = v :> { a : A & P a } := f_equal _ p. Definition projT1_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) - : projT1 u = projT1 v + : u.1 = v.1 := projT1_eq (sigT_of_sigT2_eq p). (** Projecting an equality of a pair to equality of the second components *) Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) - : rew projT1_of_sigT2_eq p in projT2 u = projT2 v + : rew projT1_of_sigT2_eq p in u.2 = v.2 := rew dependent p in eq_refl. (** Projecting an equality of a pair to equality of the third components *) @@ -443,8 +480,8 @@ Section sigT2. (** Equality of [sigT2] is itself a [sigT2] (backwards-reasoning version) *) Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) - (pqr : { p : projT1 u = projT1 v - & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }) + (pqr : { p : u.1 = v.1 + & rew p in u.2 = v.2 & rew p in projT3 u = projT3 v }) : u = v. Proof. destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *. @@ -453,8 +490,8 @@ Section sigT2. (** Curried version of proving equality of sigma types *) Definition eq_sigT2 {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) - (p : projT1 u = projT1 v) - (q : rew p in projT2 u = projT2 v) + (p : u.1 = v.1) + (q : rew p in u.2 = v.2) (r : rew p in projT3 u = projT3 v) : u = v := eq_sigT2_uncurried u v (existT2 _ _ p q r). @@ -472,8 +509,8 @@ Section sigT2. Definition eq_sigT2_uncurried_iff {A P Q} (u v : { a : A & P a & Q a }) : u = v - <-> { p : projT1 u = projT1 v - & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }. + <-> { p : u.1 = v.1 + & rew p in u.2 = v.2 & rew p in projT3 u = projT3 v }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT2_uncurried ]. Defined. @@ -498,7 +535,7 @@ Section sigT2. (** Non-dependent classification of equality of [sigT] *) Definition eq_sigT2_nondep {A B C : Type} (u v : { a : A & B & C }) - (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v) + (p : u.1 = v.1) (q : u.2 = v.2) (r : projT3 u = projT3 v) : u = v := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r). @@ -510,8 +547,8 @@ Section sigT2. = existT2 (Q y) (R y) - (rew H in projT1 u) - (rew dependent H in projT2 u) + (rew H in u.1) + (rew dependent H in u.2) (rew dependent H in projT3 u). Proof. destruct H, u; reflexivity. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index ca5f154e95..4614d215eb 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1023,6 +1023,18 @@ Proof. intros; rewrite H by intuition; rewrite IHl; auto. Qed. +Lemma ext_in_map : + forall (A B : Type)(f g:A->B) l, map f l = map g l -> forall a, In a l -> f a = g a. +Proof. induction l; intros [=] ? []; subst; auto. Qed. + +Arguments ext_in_map [A B f g l]. + +Lemma map_ext_in_iff : + forall (A B : Type)(f g:A->B) l, map f l = map g l <-> forall a, In a l -> f a = g a. +Proof. split; [apply ext_in_map | apply map_ext_in]. Qed. + +Arguments map_ext_in_iff [A B f g l]. + Lemma map_ext : forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l. Proof. @@ -1717,6 +1729,32 @@ Section Cutting. end end. + Lemma firstn_skipn_comm : forall m n l, + firstn m (skipn n l) = skipn n (firstn (n + m) l). + Proof. now intros m; induction n; intros []; simpl; destruct m. Qed. + + Lemma skipn_firstn_comm : forall m n l, + skipn m (firstn n l) = firstn (n - m) (skipn m l). + Proof. now induction m; intros [] []; simpl; rewrite ?firstn_nil. Qed. + + Lemma skipn_O : forall l, skipn 0 l = l. + Proof. reflexivity. Qed. + + Lemma skipn_nil : forall n, skipn n ([] : list A) = []. + Proof. now intros []. Qed. + + Lemma skipn_cons n a l: skipn (S n) (a::l) = skipn n l. + Proof. reflexivity. Qed. + + Lemma skipn_none : forall l, skipn (length l) l = []. + Proof. now induction l. Qed. + + Lemma skipn_all2 n: forall l, length l <= n -> skipn n l = []. + Proof. + intros l L%Nat.sub_0_le; rewrite <-(firstn_all l) at 1. + now rewrite skipn_firstn_comm, L. + Qed. + Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l. Proof. induction n. @@ -1730,6 +1768,51 @@ Section Cutting. induction n; destruct l; simpl; auto. Qed. + Lemma skipn_length n : + forall l, length (skipn n l) = length l - n. + Proof. + induction n. + - intros l; simpl; rewrite Nat.sub_0_r; reflexivity. + - destruct l; simpl; auto. + Qed. + + Lemma skipn_all l: skipn (length l) l = nil. + Proof. now induction l. Qed. + + Lemma skipn_app n : forall l1 l2, + skipn n (l1 ++ l2) = (skipn n l1) ++ (skipn (n - length l1) l2). + Proof. induction n; auto; intros [|]; simpl; auto. Qed. + + Lemma firstn_skipn_rev: forall x l, + firstn x l = rev (skipn (length l - x) (rev l)). + Proof. + intros x l; rewrite <-(firstn_skipn x l) at 3. + rewrite rev_app_distr, skipn_app, rev_app_distr, rev_length, + skipn_length, Nat.sub_diag; simpl; rewrite rev_involutive. + rewrite <-app_nil_r at 1; f_equal; symmetry; apply length_zero_iff_nil. + repeat rewrite rev_length, skipn_length; apply Nat.sub_diag. + Qed. + + Lemma firstn_rev: forall x l, + firstn x (rev l) = rev (skipn (length l - x) l). + Proof. + now intros x l; rewrite firstn_skipn_rev, rev_involutive, rev_length. + Qed. + + Lemma skipn_rev: forall x l, + skipn x (rev l) = rev (firstn (length l - x) l). + Proof. + intros x l; rewrite firstn_skipn_rev, rev_involutive, <-rev_length. + destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. + - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. + now rewrite L, Nat.sub_0_r, skipn_none. + - replace (length (rev l) - (length (rev l) - x)) + with (length (rev l) + x - length (rev l)). + rewrite minus_plus. reflexivity. + rewrite <- (Nat.sub_add _ _ L) at 2. + now rewrite <-!(Nat.add_comm x), <-minus_plus_simpl_l_reverse. + Qed. + Lemma removelast_firstn : forall n l, n < length l -> removelast (firstn (S n) l) = firstn n l. Proof. @@ -2073,6 +2156,14 @@ Section NatSeq. rewrite in_seq. intros (H,_). apply (Lt.lt_irrefl _ H). Qed. + Lemma seq_app : forall len1 len2 start, + seq start (len1 + len2) = seq start len1 ++ seq (start + len1) len2. + Proof. + induction len1 as [|len1' IHlen]; intros; simpl in *. + - now rewrite Nat.add_0_r. + - now rewrite Nat.add_succ_r, IHlen. + Qed. + End NatSeq. Section Exists_Forall. diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index ab60920fbc..691f37b414 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -92,41 +92,6 @@ module Aux = struct | None -> DirMap.remove key map | Some x -> DirMap.add key x map - (* Available in OCaml >= 4.04 *) - let split_on_char sep s = - let open String in - let r = ref [] in - let j = ref (length s) in - for i = length s - 1 downto 0 do - if unsafe_get s i = sep then begin - r := sub s (i + 1) (!j - i - 1) :: !r; - j := i - end - done; - sub s 0 !j :: !r - - (* Available in OCaml >= 4.04 *) - let is_dir_sep = match Sys.os_type with - | "Win32" -> fun s i -> s.[i] = '\\' - | _ -> fun s i -> s.[i] = '/' - - let extension_len name = - let rec check i0 i = - if i < 0 || is_dir_sep name i then 0 - else if name.[i] = '.' then check i0 (i - 1) - else String.length name - i0 - in - let rec search_dot i = - if i < 0 || is_dir_sep name i then 0 - else if name.[i] = '.' then check i (i - 1) - else search_dot (i - 1) - in - search_dot (String.length name - 1) - - let remove_extension name = - let l = extension_len name in - if l = 0 then name else String.sub name 0 (String.length name - l) - end let add_map_list key elem map = @@ -205,18 +170,18 @@ let pp_vo_dep dir fmt vo = (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) let deps = List.map (fun s -> sdir ^ s) (edep @ vo.deps) in (* The source file is also corrected as we will call coqtop from the top dir *) - let source = String.concat "/" dir ^ "/" ^ Legacy.(remove_extension vo.target) ^ ".v" in + let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in (* The final build rule *) let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in pp_rule fmt [vo.target] deps action let pp_ml4_dep _dir fmt ml = - let target = Legacy.(remove_extension ml) ^ ".ml" in + let target = Filename.(remove_extension ml) ^ ".ml" in let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in pp_rule fmt [target] [ml] ml4_rule let pp_mlg_dep _dir fmt ml = - let target = Legacy.(remove_extension ml) ^ ".ml" in + let target = Filename.(remove_extension ml) ^ ".ml" in let ml4_rule = "(run coqpp %{pp-file})" in pp_rule fmt [target] [ml] ml4_rule @@ -274,7 +239,7 @@ let parse_coqdep_line l = begin match targets with | [target] -> let dir, target = Filename.(dirname target, basename target) in - Some (Legacy.split_on_char '/' dir, VO { target; deps; }) + Some (String.split_on_char '/' dir, VO { target; deps; }) (* Otherwise a vio file, we ignore *) | _ -> None end diff --git a/vernac/classes.ml b/vernac/classes.ml index e491761aec..c738d14af9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -121,19 +121,167 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in - let entry = - Declare.definition_entry ~types:termtype ~univs:uctx term - in + let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in - Declare.definition_message id; - Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); - instance_hook k info global imps ?hook (ConstRef kn); - id + Declare.definition_message id; + Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); + instance_hook k info global imps ?hook (ConstRef kn) + +let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id = + let subst = List.fold_left2 + (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') + [] subst (snd k.cl_context) + in + let (_, ty_constr) = instance_constructor (k,u) subst in + let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in + let sigma = Evd.minimize_universes sigma in + Pretyping.check_evars env (Evd.from_env env) sigma termtype; + let univs = Evd.check_univ_decl ~poly sigma decl in + let termtype = to_constr sigma termtype in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id + (ParameterEntry + (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + in + Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); + instance_hook k pri global imps ?hook (ConstRef cst); id -let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) - ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) - ?(tac:unit Proofview.tactic option) ?hook pri = +let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = + let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in + if program_mode then + let hook vis gr _ = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + Impargs.declare_manual_implicits false gr ~enriching:false [imps]; + let pri = intern_info pri in + Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) + in + let obls, constr, typ = + match term with + | Some t -> + let obls, _, constr, typ = + Obligations.eterm_obligations env id sigma 0 t termtype + in obls, Some constr, typ + | None -> [||], None, termtype + in + let hook = Lemmas.mk_hook hook in + let ctx = Evd.evar_universe_context sigma in + ignore (Obligations.add_definition id ?term:constr + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) + else + Flags.silently (fun () -> + (* spiwack: it is hard to reorder the actions to do + the pretyping after the proof has opened. As a + consequence, we use the low-level primitives to code + the refinement manually.*) + let gls = List.rev (Evd.future_goals sigma) in + let sigma = Evd.reset_future_goals sigma in + Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) + (Lemmas.mk_hook + (fun _ -> instance_hook k pri global imps ?hook)); + (* spiwack: I don't know what to do with the status here. *) + if not (Option.is_empty term) then + let init_refine = + Tacticals.New.tclTHENLIST [ + Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); + Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); + Tactics.New.reduce_after_refine; + ] + in + ignore (Pfedit.by init_refine) + else if Flags.is_auto_intros () then + ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); + (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () + +let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len = + let props = + match props with + | Some (true, { CAst.v = CRecord fs }) -> + if List.length fs > List.length k.cl_props then + mismatched_props env' (List.map snd fs) k.cl_props; + Some (Inl fs) + | Some (_, t) -> Some (Inr t) + | None -> + if program_mode then Some (Inl []) + else None + in + let subst, sigma = + match props with + | None -> + (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma + | Some (Inr term) -> + let sigma, c = interp_casted_constr_evars env' sigma term cty in + Some (Inr (c, subst)), sigma + | Some (Inl props) -> + let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in + let props, rest = + List.fold_left + (fun (props, rest) decl -> + if is_local_assum decl then + try + let is_id (id', _) = match RelDecl.get_name decl, get_id id' with + | Name id, {CAst.v=id'} -> Id.equal id id' + | Anonymous, _ -> false + in + let (loc_mid, c) = List.find is_id rest in + let rest' = List.filter (fun v -> not (is_id v)) rest + in + let {CAst.loc;v=mid} = get_id loc_mid in + List.iter (fun (n, _, x) -> + if Name.equal n (Name mid) then + Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs; + c :: props, rest' + with Not_found -> + ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest + else props, rest) + ([], props) k.cl_props + in + match rest with + | (n, _) :: _ -> + unbound_method env' k.cl_impl (get_id n) + | _ -> + let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in + let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in + Some (Inl res), sigma + in + let term, termtype = + match subst with + | None -> let termtype = it_mkProd_or_LetIn cty ctx in + None, termtype + | Some (Inl subst) -> + let subst = List.fold_left2 + (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') + [] subst (k.cl_props @ snd k.cl_context) + in + let (app, ty_constr) = instance_constructor (k,u) subst in + let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in + let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in + Some term, termtype + | Some (Inr (def, subst)) -> + let termtype = it_mkProd_or_LetIn cty ctx in + let term = it_mkLambda_or_LetIn def ctx in + Some term, termtype + in + let sigma = Evarutil.nf_evar_map sigma in + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in + (* Try resolving fields that are typeclasses automatically. *) + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in + let sigma = Evarutil.nf_evar_map_undefined sigma in + (* Beware of this step, it is required as to minimize universes. *) + let sigma = Evd.minimize_universes sigma in + (* Check that the type is free of evars now. *) + Pretyping.check_evars env (Evd.from_env env) sigma termtype; + let termtype = to_constr sigma termtype in + let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in + if not (Evd.has_undefined sigma) && not (Option.is_empty term) then + declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype + else if program_mode || refine || Option.is_empty term then + declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype + else CErrors.user_err Pp.(str "Unsolved obligations remaining."); + id + +let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode + poly ctx (instid, bk, cl) props + ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in @@ -150,9 +298,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) cl | Explicit -> cl, Id.Set.empty in - let tclass = - if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) - else tclass + let tclass = + if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) + else tclass in let sigma, k, u, cty, ctx', ctx, len, imps, subst = let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in @@ -189,163 +337,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let env' = push_rel_context ctx env in let sigma = Evarutil.nf_evar_map sigma in let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in - if abstract then - begin - let subst = List.fold_left2 - (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') - [] subst (snd k.cl_context) - in - let (_, ty_constr) = instance_constructor (k,u) subst in - let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma = Evd.minimize_universes sigma in - Pretyping.check_evars env (Evd.from_env env) sigma termtype; - let univs = Evd.check_univ_decl ~poly sigma decl in - let termtype = to_constr sigma termtype in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry - (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) - in - Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); - instance_hook k pri global imps ?hook (ConstRef cst); id - end - else ( - let props = - match props with - | Some (true, { CAst.v = CRecord fs }) -> - if List.length fs > List.length k.cl_props then - mismatched_props env' (List.map snd fs) k.cl_props; - Some (Inl fs) - | Some (_, t) -> Some (Inr t) - | None -> - if program_mode then Some (Inl []) - else None - in - let subst, sigma = - match props with - | None -> - (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma - | Some (Inr term) -> - let sigma, c = interp_casted_constr_evars env' sigma term cty in - Some (Inr (c, subst)), sigma - | Some (Inl props) -> - let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in - let props, rest = - List.fold_left - (fun (props, rest) decl -> - if is_local_assum decl then - try - let is_id (id', _) = match RelDecl.get_name decl, get_id id' with - | Name id, {CAst.v=id'} -> Id.equal id id' - | Anonymous, _ -> false - in - let (loc_mid, c) = - List.find is_id rest - in - let rest' = - List.filter (fun v -> not (is_id v)) rest - in - let {CAst.loc;v=mid} = get_id loc_mid in - List.iter (fun (n, _, x) -> - if Name.equal n (Name mid) then - Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) - k.cl_projs; - c :: props, rest' - with Not_found -> - ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest - else props, rest) - ([], props) k.cl_props - in - match rest with - | (n, _) :: _ -> - unbound_method env' k.cl_impl (get_id n) - | _ -> - let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in - let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in - Some (Inl res), sigma - in - let term, termtype = - match subst with - | None -> let termtype = it_mkProd_or_LetIn cty ctx in - None, termtype - | Some (Inl subst) -> - let subst = List.fold_left2 - (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') - [] subst (k.cl_props @ snd k.cl_context) - in - let (app, ty_constr) = instance_constructor (k,u) subst in - let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in - Some term, termtype - | Some (Inr (def, subst)) -> - let termtype = it_mkProd_or_LetIn cty ctx in - let term = it_mkLambda_or_LetIn def ctx in - Some term, termtype - in - let sigma = Evarutil.nf_evar_map sigma in - let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in - (* Try resolving fields that are typeclasses automatically. *) - let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in - let sigma = Evarutil.nf_evar_map_undefined sigma in - (* Beware of this step, it is required as to minimize universes. *) - let sigma = Evd.minimize_universes sigma in - (* Check that the type is free of evars now. *) - Pretyping.check_evars env (Evd.from_env env) sigma termtype; - let termtype = to_constr sigma termtype in - let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in - if not (Evd.has_undefined sigma) && not (Option.is_empty term) then - declare_instance_constant k pri global imps ?hook id decl - poly sigma (Option.get term) termtype - else if program_mode || refine || Option.is_empty term then begin - let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in - if program_mode then - let hook vis gr _ = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr ~enriching:false [imps]; - let pri = intern_info pri in - Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) - in - let obls, constr, typ = - match term with - | Some t -> - let obls, _, constr, typ = - Obligations.eterm_obligations env id sigma 0 t termtype - in obls, Some constr, typ - | None -> [||], None, termtype - in - let hook = Lemmas.mk_hook hook in - let ctx = Evd.evar_universe_context sigma in - ignore (Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls); - id - else - (Flags.silently - (fun () -> - (* spiwack: it is hard to reorder the actions to do - the pretyping after the proof has opened. As a - consequence, we use the low-level primitives to code - the refinement manually.*) - let gls = List.rev (Evd.future_goals sigma) in - let sigma = Evd.reset_future_goals sigma in - Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) - (Lemmas.mk_hook - (fun _ -> instance_hook k pri global imps ?hook)); - (* spiwack: I don't know what to do with the status here. *) - if not (Option.is_empty term) then - let init_refine = - Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); - Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); - Tactics.New.reduce_after_refine; - ] - in - ignore (Pfedit.by init_refine) - else if Flags.is_auto_intros () then - ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); - (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) (); - id) - end - else CErrors.user_err Pp.(str "Unsolved obligations remaining.")) - + if abstract then + do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id + else + do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode + cty k u ctx ctx' pri decl imps subst id props len + let named_of_rel_context l = let open Vars in let acc, ctx = @@ -433,5 +430,5 @@ let context poly l = Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus - in + in List.fold_left fn true (List.rev ctx) diff --git a/vernac/classes.mli b/vernac/classes.mli index 9c37364cb0..bb70334342 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -37,7 +37,7 @@ val declare_instance_constant : Evd.evar_map -> (* Universes *) Constr.t -> (** body *) Constr.types -> (** type *) - Names.Id.t + unit val new_instance : ?abstract:bool -> (** Not abstract by default. *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 3ee836a828..b354ad0521 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -82,7 +82,7 @@ let _ = let is_eq_flag () = !eq_flag -let eq_dec_flag = ref false +let eq_dec_flag = ref false let _ = declare_bool_option { optdepr = false; @@ -383,7 +383,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = and env0 = Global.env() in let sigma, lrecspec, _ = List.fold_right - (fun (_,dep,ind,sort) (evd, l, inst) -> + (fun (_,dep,ind,sort) (evd, l, inst) -> let evd, indu, inst = match inst with | None -> @@ -454,6 +454,9 @@ let fold_left' f = function let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ()) let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ()) +let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.build_coq_prod ()) +let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.build_coq_pair ()) + let build_combined_scheme env schemes = let evdref = ref (Evd.from_env env) in let defs = List.map (fun cst -> @@ -471,10 +474,25 @@ let build_combined_scheme env schemes = in let (c, t) = List.hd defs in let ctx, ind, nargs = find_inductive t in + (* We check if ALL the predicates are in Prop, if so we use propositional + conjunction '/\', otherwise we use the simple product '*'. + *) + let inprop = + let inprop (_,t) = + Retyping.get_sort_family_of env !evdref (EConstr.of_constr t) + == Sorts.InProp + in + List.for_all inprop defs + in + let mk_and, mk_conj = + if inprop + then (mk_coq_and, mk_coq_conj) + else (mk_coq_prod, mk_coq_pair) + in (* Number of clauses, including the predicates quantification *) let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in - let sigma, coqand = mk_coq_and !evdref in - let sigma, coqconj = mk_coq_conj sigma in + let sigma, coqand = mk_and !evdref in + let sigma, coqconj = mk_conj sigma in let () = evdref := sigma in let relargs = rel_vect 0 prods in let concls = List.rev_map @@ -492,7 +510,8 @@ let build_combined_scheme env schemes = (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in - (!evdref, body, typ) + let sigma = Typing.check env !evdref (EConstr.of_constr body) (EConstr.of_constr typ) in + (sigma, body, typ) let do_combined_scheme name schemes = let open CAst in diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d25dea1413..3620e177fe 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -69,9 +69,6 @@ type kind_load = (* Must be always initialized *) let load = ref WithoutTop -(* Are we in a native version of Coq? *) -let is_native = Dynlink.is_native - (* Sets and initializes a toplevel (if any) *) let set_top toplevel = load := WithTop toplevel; @@ -89,7 +86,7 @@ let is_ocaml_top () = |_ -> false (* Tests if we can load ML files *) -let has_dynlink = Coq_config.has_natdynlink || not is_native +let has_dynlink = Coq_config.has_natdynlink || not Sys.(backend_type = Native) (* Runs the toplevel loop of Ocaml *) let ocaml_toploop () = @@ -149,7 +146,7 @@ let dir_ml_use s = | WithTop t -> t.use_file s | _ -> let moreinfo = - if Dynlink.is_native then " Loading ML code works only in bytecode." + if Sys.(backend_type = Native) then " Loading ML code works only in bytecode." else "" in user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) @@ -257,7 +254,8 @@ let file_of_name name = str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in if not (Filename.is_relative name) then if Sys.file_exists name then name else fail name - else if is_native then + else if Sys.(backend_type = Native) then + (* XXX: Dynlink.adapt_filename does the same? *) let name = match suffix with | Some ((".cmo"|".cma") as suffix) -> (Filename.chop_suffix name suffix) ^ ".cmxs" diff --git a/vernac/mltop.mli b/vernac/mltop.mli index ed1f9a12d8..3d796aa4aa 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -21,9 +21,6 @@ type toplevel = { (** Sets and initializes a toplevel (if any) *) val set_top : toplevel -> unit -(** Are we in a native version of Coq? *) -val is_native : bool - (** Removes the toplevel (if any) *) val remove : unit -> unit |
