diff options
60 files changed, 648 insertions, 272 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ae55302d11..d2e335d45a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -60,6 +60,7 @@ before_script: paths: - _install_ci - config/Makefile + - test-suite/misc/universes/all_stdlib.v expire_in: 1 week script: - set -e @@ -70,6 +71,7 @@ before_script: - echo 'start:coq.build' - make -j ${NJOBS} + - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' - echo 'start:coq.install' diff --git a/.travis.yml b/.travis.yml index 6c926aacbd..1a9f6964f7 100644 --- a/.travis.yml +++ b/.travis.yml @@ -31,6 +31,7 @@ env: # system is == 4.02.3 - COMPILER="system" - CAMLP5_VER="6.14" + - FINDLIB_VER="1.4.1" - NATIVE_COMP="yes" - COQ_DEST="-local" # Main test suites @@ -62,9 +63,6 @@ env: matrix: - allow_failures: - - env: TEST_TARGET="ci-geocoq TIMED=1" - include: # Full Coq test-suite with two compilers - env: @@ -95,6 +93,7 @@ matrix: - env: - TEST_TARGET="test-suite" - COMPILER="4.05.0" + - FINDLIB_VER="1.7.3" - CAMLP5_VER="7.01" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="lablgtk-extras hevea" @@ -125,6 +124,7 @@ matrix: - TEST_TARGET="coqocaml" - COMPILER="4.05.0" - CAMLP5_VER="7.01" + - FINDLIB_VER="1.7.3" - EXTRA_CONF="-coqide opt -warn-error" - EXTRA_OPAM="lablgtk-extras hevea" # dummy target @@ -140,7 +140,7 @@ matrix: env: - TEST_TARGET="test-suite" - COMPILER="4.02.3" - - CAMLP5_VER="6.17" + - CAMLP5_VER="6.17" - NATIVE_COMP="no" - COQ_DEST="-local" before_install: @@ -173,14 +173,6 @@ matrix: skip_cleanup: true on: all_branches: true - - provider: releases - api_key: - secure: "Z/ewvydCLXEhlBBtQGYm2nZ8o+2RP+MwA5uEDuu6mEpZttUZAYaoHivChxADLXz8LNKvUloIeBeIL/PrLk6QnhSur/s2iEYHssrnl99SkAPtoWggyfsdacuKLMkpLoZGOBIEYKPuXuEZyqvugSUO42rSya1zdjcnXc4l+E/bXMc=" - file: _build/*.dmg - skip_cleanup: true - on: - tags: true - repo: coq/coq before_install: - if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi @@ -189,7 +181,7 @@ install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config list -- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} +- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind.${FINDLIB_VER} ${EXTRA_OPAM} - opam list script: @@ -13,14 +13,22 @@ Tactics profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. -Changes from 8.7+beta1 to 8.7.0 -=============================== +Changes from 8.7+beta1 to 8.7+beta2 +=================================== Tools - In CoqIDE, the "Compile Buffer" command takes account of flags in _CoqProject or other project file. +Improvements around some error messages. + +Many bug fixes including two important ones: + +- BZ#5730: CoqIDE becomes unresponsive on file open. +- coq_makefile: make sure compile flags for Coq and coq_makefile are in sync + (in particular, make sure the `-safe-string` option is used to compile plugins). + Changes from 8.6.1 to 8.7+beta1 =============================== @@ -1,5 +1,5 @@ - INSTALLATION PROCEDURES FOR THE COQ V8.6 SYSTEM + INSTALLATION PROCEDURES FOR THE COQ V8.7 SYSTEM ----------------------------------------------- @@ -27,19 +27,16 @@ WHAT DO YOU NEED ? port install coq - To compile Coq V8.6 yourself, you need: + To compile Coq V8.7 yourself, you need: - - OCaml version 4.02.1 or later - (available at http://caml.inria.fr/) + - OCaml version 4.02.3 or later + (available at https://ocaml.org/) - OCaml version 4.02.0 is not supported because of a severe performance - issue increasing compilation time. + - Findlib (version >= 1.4.1) + (available at http://projects.camlcity.org/projects/findlib.html) - - Findlib (included in OCaml binary distribution under windows, - probably available in your distribution and for sure at - http://projects.camlcity.org/projects/findlib.html) - - - Camlp5 (version >= 6.02) + - Camlp5 (version >= 6.14) + (available at https://camlp5.github.io/) - GNU Make version 3.81 or later @@ -48,6 +45,12 @@ WHAT DO YOU NEED ? - for Coqide, the Lablgtk development files, and the GTK libraries incuding gtksourceview, see INSTALL.ide for more details + Opam (https://opam.ocaml.org/) is recommended to install ocaml and + the corresponding packages. + + $ opam install ocamlfind camlp5 lablgtk-extras + + should get you a reasonable OCaml environment to compile Coq. QUICK INSTALLATION PROCEDURE. ============================= diff --git a/Makefile.build b/Makefile.build index 26a40c6cc1..ecaaccaafe 100644 --- a/Makefile.build +++ b/Makefile.build @@ -195,8 +195,8 @@ MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) -BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS) -OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) +BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) +OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$<),, -I ide -I ide/utils) # On MacOS, the binaries are signed, except our private ones @@ -429,6 +429,7 @@ tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # is being built. COQDEPBOOTSRC := lib/minisys.cmo \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo \ tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo tools/coqdep_lexer.cmo : tools/coqdep_lexer.cmi @@ -449,6 +450,7 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) # The full coqdep (unused by this build, but distributed by make install) COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo lib/minisys.cmo \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo \ lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \ tools/coqdep.cmo diff --git a/config/coq_config.mli b/config/coq_config.mli index b0f39e9d28..429d8811bd 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -36,6 +36,7 @@ val camlp4compat : string (* compatibility argument to camlp4/5 *) val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *) val cflags : string (* arguments passed to gcc *) +val caml_flags : string (* arguments passed to ocamlc (ie. CAMLFLAGS) *) val best : string (* byte/opt *) val arch : string (* architecture *) diff --git a/configure.ml b/configure.ml index b5e4567792..fc2233f78d 100644 --- a/configure.ml +++ b/configure.ml @@ -263,10 +263,6 @@ module Prefs = struct let debug = ref true let profile = ref false let annotate = ref false - (* Note, disabling this should be OK, but be careful with the - sharing invariants. - *) - let safe_string = ref true let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) let coqwebsite = ref "http://coq.inria.fr/" let force_caml_version = ref false @@ -376,8 +372,9 @@ let coq_annotate_flag = then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot" else "" -let coq_safe_string = - if !Prefs.safe_string then "-safe-string" else "" +(* This variable can be overriden only for debug purposes, use with + care. *) +let coq_safe_string = "-safe-string" let cflags = "-Wall -Wno-unused -g -O2" @@ -512,19 +509,22 @@ let camltag = match caml_version_list with 50: unexpected documentation comment: too common and annoying to avoid 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 *) -let coq_warn_flags = - let warnings = "-w +a-4-9-27-41-42-44-45-48-50" in - let errors = +let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50" +let coq_warn_error = if !Prefs.warn_error then "-warn-error +a" ^ (if caml_version_nums > [4;2;3] then "-56" else "") else "" - in - warnings ^ " " ^ errors +(* Flags used to compile Coq and plugins (via coq_makefile) *) +let caml_flags = + Printf.sprintf "-thread -rectypes %s %s %s" coq_warnings coq_annotate_flag coq_safe_string +(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *) +let coq_caml_flags = + coq_warn_error (** * CamlpX configuration *) @@ -1050,6 +1050,7 @@ let write_configml f = pr_s "camlp4lib" camlpXlibdir; pr_s "camlp4compat" camlp4compat; pr_s "cflags" cflags; + pr_s "caml_flags" caml_flags; pr_s "best" best_compiler; pr_s "osdeplibs" osdeplibs; pr_s "version" coq_version; @@ -1156,7 +1157,7 @@ let write_makefile f = pr "CAMLHLIB=%S\n\n" camllib; pr "# Caml link command and Caml make top command\n"; pr "# Caml flags\n"; - pr "CAMLFLAGS=-rectypes %s %s %s\n" coq_warn_flags coq_annotate_flag coq_safe_string; + pr "CAMLFLAGS=%s %s\n" caml_flags coq_caml_flags; pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; pr "# Flags for GCC\n"; diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index eadeb7c38c..8e6448e764 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -8,9 +8,5 @@ GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} ( cd ${GeoCoq_CI_DIR} && \ - ./configure.sh && \ - sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ - sed -i.bak '/Elements\/Book_1\.v/d' Make && \ - sed -i.bak '/Elements\/Book_3\.v/d' Make && \ - coq_makefile -f Make -o Makefile && \ + ./configure-ci.sh && \ make ) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 5ed74917aa..b5e19f33c3 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -641,6 +641,12 @@ The main search functions now take a function iterating over the results. This allows for clients to use streaming or more economic printing. +### XML Protocol + +- In several places, flat text wrapped in `<string>` tags now appears as structured text inside `<richpp>` tags. + +- The "errormsg" feedback has been replaced by a "message" feedback which contains `<feedback\_content>` tag, with a message_level attribute of "error". + ## Changes between Coq 8.4 and Coq 8.5 ### Refactoring : more mli interfaces and simpler grammar.cma diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index cf7d205d8b..18f6288f6f 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -1,4 +1,4 @@ -#Coq XML Protocol for Coq 8.6# +# Coq XML Protocol This document is based on documentation originally written by CJ Bell for his [vscoq](https://github.com/siegebell/vscoq/) project. @@ -12,11 +12,7 @@ A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). -# CHANGES -## Changes from 8.5: - * In several places, flat text wrapped in <string> tags now appears as structured text inside <richpp> tags - * The "errormsg" feedback has been replaced by a "message" feedback which contains - <feedback\_content> tag, with a message_level attribute of "error" +Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt). * [Commands](#commands) - [About](#command-about) diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index 1c415eca69..5d151381ff 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -52,20 +52,7 @@ <h2 style="text-align:center; font-size: 150%">The Coq Development Team</h2> <br /><br /><br /> -<div style="text-align: left; font-size: 80%; text-indent: 0pt"> -<ul style="list-style: none; margin-left: 0pt"> - <li>V7.x © INRIA 1999-2004</li> - <li>V8.0 © INRIA 2004-2008</li> - <li>V8.1 © INRIA 2006-2011</li> - <li>V8.2 © INRIA 2008-2011</li> - <li>V8.3 © INRIA 2010-2011</li> - <li>V8.4 © INRIA 2012-2014</li> - <li>V8.5 © INRIA 2015-2016</li> - <li>V8.6 © INRIA 2016</li> -</ul> - -<p style="text-indent:0pt">This research was partly supported by IST - working group ``Types''</p> +<p style="text-indent:0pt">Copyright © INRIA 1999-2017</p> <p style="text-indent:0pt">This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <a href="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</a>). Options A and B are not elected.</p> diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html index 25fb56320b..6053131045 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -30,20 +30,7 @@ <br /><br /><br /> -<div style="text-align: left; font-size: 80%; text-indent: 0pt"> -<ul style="list-style: none; margin-left: 0pt"> - <li>V7.x © INRIA 1999-2004</li> - <li>V8.0 © INRIA 2004-2008</li> - <li>V8.1 © INRIA 2006-2011</li> - <li>V8.2 © INRIA 2008-2011</li> - <li>V8.3 © INRIA 2010-2011</li> - <li>V8.4 © INRIA 2012-2014</li> - <li>V8.5 © INRIA 2015-2016</li> - <li>V8.6 © INRIA 2016</li> -</ul> - -<p style="text-indent:0pt">This research was partly supported by IST - working group ``Types''</p> +<p style="text-indent:0pt">Copyright © INRIA 1999-2017</p> <p style="text-indent: 0pt">This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <a href="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</a>). Options A and B are not elected.</p> diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 9790111f14..892c9931b6 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -107,6 +107,15 @@ The following command-line options are recognized by the commands {\tt recursively available from {\Coq} using absolute names (extending the {\dirpath} prefix) (see Section~\ref{LongNames}). + Note that only those subdirectories and files which obey the lexical + conventions of what is an {\ident} (see Section~\ref{lexical}) + are taken into account. Conversely, the underlying file systems or + operating systems may be more restrictive than {\Coq}. While Linux's + ext4 file system supports any {\Coq} recursive layout + (within the limit of 255 bytes per file name), the default on NTFS + (Windows) or HFS+ (MacOS X) file systems is on the contrary to + disallow two files differing only in the case in the same directory. + \SeeAlso Section~\ref{Libraries}. \item[{\tt -R} {\em directory} {\dirpath}]\ % diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 339c6a248e..eabfb7b398 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -478,8 +478,6 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error -let cleared = Store.field () - exception Depends of Id.t let rec check_and_clear_in_constr env evdref err ids global c = @@ -552,13 +550,6 @@ let rec check_and_clear_in_constr env evdref err ids global c = let evd = !evdref in let (evd,_) = restrict_evar evd evk filter None in evdref := evd; - (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) - let evi = Evd.find !evdref evk in - let extra = evi.evar_extra in - let extra' = Store.set extra cleared true in - let evi' = { evi with evar_extra = extra' } in - evdref := Evd.add !evdref evk evi' ; - (* spiwack: /hacking session *) Evd.existential_value !evdref ev | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c @@ -665,11 +656,9 @@ let rec advance sigma evk = match evi.evar_body with | Evar_empty -> Some evk | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra cleared) then - let (evk,_) = Term.destEvar v in - advance sigma evk - else - None + match is_restricted_evar evi with + | Some evk -> advance sigma evk + | None -> None (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 14173e774d..ee0fae3d46 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -204,10 +204,6 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error -(* spiwack: marks an evar that has been "defined" by clear. - used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) -val cleared : bool Store.field - val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> Id.Set.t -> named_context_val * types diff --git a/engine/evd.ml b/engine/evd.ml index f1b5419dec..324f883e8e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -630,7 +630,9 @@ let evar_source evk d = (find d evk).evar_source let evar_ident evk evd = EvNames.ident evk evd.evar_names let evar_key id evd = EvNames.key id evd.evar_names -let define_aux def undef evk body = +let restricted = Store.field () + +let define_aux ?dorestrict def undef evk body = let oldinfo = try EvMap.find evk undef with Not_found -> @@ -640,7 +642,10 @@ let define_aux def undef evk body = anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") in let () = assert (oldinfo.evar_body == Evar_empty) in - let newinfo = { oldinfo with evar_body = Evar_defined body } in + let evar_extra = match dorestrict with + | Some evk' -> Store.set oldinfo.evar_extra restricted evk' + | None -> oldinfo.evar_extra in + let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in EvMap.add evk newinfo def, EvMap.remove evk undef (* define the existential of section path sp as the constr body *) @@ -653,6 +658,9 @@ let define evk body evd = let evar_names = EvNames.remove_name_defined evk evd.evar_names in { evd with defn_evars; undf_evars; last_mods; evar_names } +let is_restricted_evar evi = + Store.get evi.evar_extra restricted + let restrict evk filter ?candidates ?src evd = let evk' = new_untyped_evar () in let evar_info = EvMap.find evk evd.undf_evars in @@ -667,7 +675,7 @@ let restrict evk filter ?candidates ?src evd = let ctxt = Filter.filter_list filter (evar_context evar_info) in let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in let body = mkEvar(evk',id_inst) in - let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in + let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; defn_evars; last_mods; evar_names }, evk' diff --git a/engine/evd.mli b/engine/evd.mli index abcabe8157..9055dcc86b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -244,6 +244,9 @@ val restrict : evar -> Filter.t -> ?candidates:constr list -> (** Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates *) +val is_restricted_evar : evar_info -> evar option +(** Tell if an evar comes from restriction of another evar, and if yes, which *) + val downcast : evar -> types -> evar_map -> evar_map (** Change the type of an undefined evar to a new type assumed to be a subtype of its current type; subtyping must be ensured by caller *) diff --git a/engine/namegen.ml b/engine/namegen.ml index 1dd29e6eae..2e62b89011 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -43,6 +43,8 @@ let default_non_dependent_ident = Id.of_string default_non_dependent_string let default_dependent_ident = Id.of_string "x" +let default_generated_non_letter_string = "x" + (**********************************************************************) (* Globality of identifiers *) @@ -107,7 +109,17 @@ let head_name sigma c = (* Find the head constant of a constr if any *) hdrec c let lowercase_first_char id = (* First character of a constr *) - Unicode.lowercase_first_char (Id.to_string id) + let s = Id.to_string id in + match Unicode.split_at_first_letter s with + | None -> + (* General case: nat -> n *) + Unicode.lowercase_first_char s + | Some (s,s') -> + if String.length s' = 0 then + (* No letter, e.g. __, or __'_, etc. *) + default_generated_non_letter_string + else + s ^ Unicode.lowercase_first_char s' let sort_hdchar = function | Prop(_) -> "P" diff --git a/engine/proofview.ml b/engine/proofview.ml index eef2b83f44..598358c472 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -153,8 +153,12 @@ let focus i j sp = ( { sp with comb = new_comb } , context ) (** [undefined defs l] is the list of goals in [l] which are still - unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (Evarutil.advance defs) l + unsolved (after advancing cleared goals). Note that order matters. *) +let undefined defs l = + List.fold_right (fun evk l -> + match Evarutil.advance defs evk with + | Some evk -> List.add_set Evar.equal evk l + | None -> l) l [] (** Unfocuses a proofview with respect to a context. *) let unfocus c sp = diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index ff71452672..3699b1c614 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -93,8 +93,12 @@ let split_flags s = "all" flag, and reverses the list. *) let rec cut_before_all_rev acc = function | [] -> acc - | (_status,name as w) :: warnings -> - cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings + | (status,name as w) :: warnings -> + let acc = + if is_all_keyword name then [w] + else if is_none_keyword name then [(Disabled,"all")] + else w :: acc in + cut_before_all_rev acc warnings let cut_before_all_rev warnings = cut_before_all_rev [] warnings diff --git a/lib/envars.ml b/lib/envars.ml index 68604ae6c9..206d750338 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -213,6 +213,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ()); fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ()); fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat; + fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) @@ -82,10 +82,21 @@ let utf8_length s = done ; !cnt -let app s1 s2 = match s1, s2 with - | Ppcmd_empty, s - | s, Ppcmd_empty -> s - | s1, s2 -> Ppcmd_glue [s1; s2] +let rec app d1 d2 = match d1, d2 with + | Ppcmd_empty, d + | d, Ppcmd_empty -> d + + (* Optimizations *) + | Ppcmd_glue [l1;l2], Ppcmd_glue l3 -> Ppcmd_glue (l1 :: l2 :: l3) + | Ppcmd_glue [l1;l2], d2 -> Ppcmd_glue [l1 ; l2 ; d2] + | d1, Ppcmd_glue l2 -> Ppcmd_glue (d1 :: l2) + + | Ppcmd_tag(t1,d1), Ppcmd_tag(t2,d2) + when t1 = t2 -> Ppcmd_tag(t1,app d1 d2) + | d1, d2 -> Ppcmd_glue [d1; d2] + (* Optimizations deemed too costly *) + (* | Ppcmd_glue l1, Ppcmd_glue l2 -> Ppcmd_glue (l1 @ l2) *) + (* | Ppcmd_string s1, Ppcmd_string s2 -> Ppcmd_string (s1 ^ s2) *) let seq s = Ppcmd_glue s diff --git a/lib/system.ml b/lib/system.ml index 12eacf2eaf..0b64b237da 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -52,7 +52,7 @@ let dirmap = ref StrMap.empty let make_dir_table dir = let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in - Array.fold_left filter_dotfiles StrSet.empty (readdir dir) + Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) let exists_in_dir_respecting_case dir bf = let cache_dir dir = diff --git a/lib/unicode.ml b/lib/unicode.ml index 959ccaf73c..f193c4e0f8 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -8,13 +8,14 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol | Unknown +type status = Letter | IdentPart | Symbol | IdentSep | Unknown (* The following table stores classes of Unicode characters that - are used by the lexer. There are 3 different classes so 2 bits are - allocated for each character. We only use 16 bits over the 31 bits - to simplify the masking process. (This choice seems to be a good - trade-off between speed and space after some benchmarks.) *) + are used by the lexer. There are 5 different classes so 3 bits + are allocated for each character. We encode the masks of 8 + characters per word, thus using 24 bits over the 31 available + bits. (This choice seems to be a good trade-off between speed + and space after some benchmarks.) *) (* A 256 KiB table, initially filled with zeros. *) let table = Array.make (1 lsl 17) 0 @@ -24,14 +25,15 @@ let table = Array.make (1 lsl 17) 0 define the position of the pattern in the word. Notice that pattern "00" means "undefined". *) let mask i = function - | Letter -> 1 lsl ((i land 7) lsl 1) (* 01 *) - | IdentPart -> 2 lsl ((i land 7) lsl 1) (* 10 *) - | Symbol -> 3 lsl ((i land 7) lsl 1) (* 11 *) - | Unknown -> 0 lsl ((i land 7) lsl 1) (* 00 *) + | Letter -> 1 lsl ((i land 7) * 3) (* 001 *) + | IdentPart -> 2 lsl ((i land 7) * 3) (* 010 *) + | Symbol -> 3 lsl ((i land 7) * 3) (* 011 *) + | IdentSep -> 4 lsl ((i land 7) * 3) (* 100 *) + | Unknown -> 0 lsl ((i land 7) * 3) (* 000 *) -(* Helper to reset 2 bits in a word. *) +(* Helper to reset 3 bits in a word. *) let reset_mask i = - lnot (3 lsl ((i land 7) lsl 1)) + lnot (7 lsl ((i land 7) * 3)) (* Initialize the lookup table from a list of segments, assigning a status to every character of each segment. The order of these @@ -50,13 +52,14 @@ let mk_lookup_table_from_unicode_tables_for status tables = (* Look up into the table and interpret the found pattern. *) let lookup x = - let v = (table.(x lsr 3) lsr ((x land 7) lsl 1)) land 3 in + let v = (table.(x lsr 3) lsr ((x land 7) * 3)) land 7 in if v = 1 then Letter else if v = 2 then IdentPart else if v = 3 then Symbol + else if v = 4 then IdentSep else Unknown -(* [classify] discriminates between 3 different kinds of +(* [classify] discriminates between 5 different kinds of symbols based on the standard unicode classification (extracted from Camomile). *) let classify = @@ -67,13 +70,13 @@ let classify = Unicodetable.sm; (* Symbol, maths. *) Unicodetable.sc; (* Symbol, currency. *) Unicodetable.so; (* Symbol, modifier. *) - Unicodetable.pd; (* Punctation, dash. *) - Unicodetable.pc; (* Punctation, connector. *) - Unicodetable.pe; (* Punctation, open. *) - Unicodetable.ps; (* Punctation, close. *) - Unicodetable.pi; (* Punctation, initial quote. *) - Unicodetable.pf; (* Punctation, final quote. *) - Unicodetable.po; (* Punctation, other. *) + Unicodetable.pd; (* Punctuation, dash. *) + Unicodetable.pc; (* Punctuation, connector. *) + Unicodetable.pe; (* Punctuation, open. *) + Unicodetable.ps; (* Punctution, close. *) + Unicodetable.pi; (* Punctuation, initial quote. *) + Unicodetable.pf; (* Punctuation, final quote. *) + Unicodetable.po; (* Punctuation, other. *) ]; mk_lookup_table_from_unicode_tables_for Letter [ @@ -107,14 +110,14 @@ let classify = [(0x02074, 0x02079)]; (* Superscript 4-9. *) single 0x0002E; (* Dot. *) ]; - mk_lookup_table_from_unicode_tables_for Letter + mk_lookup_table_from_unicode_tables_for IdentSep [ single 0x005F; (* Underscore. *) single 0x00A0; (* Non breaking space. *) ]; mk_lookup_table_from_unicode_tables_for IdentPart [ - single 0x0027; (* Special space. *) + single 0x0027; (* Single quote. *) ]; (* Lookup *) lookup @@ -163,24 +166,75 @@ let is_utf8 s = in try check 0 with End_of_input -> true | Invalid_argument _ -> false +(* Escape string if it contains non-utf8 characters *) + +let escaped_non_utf8 s = + let mk_escape x = Printf.sprintf "%%%X" x in + let buff = Buffer.create (String.length s * 3) in + let rec process_trailing_aux i j = + if i = j then i else + match String.unsafe_get s i with + | '\128'..'\191' -> process_trailing_aux (i+1) j + | _ -> i in + let process_trailing i n = + let j = if i+n-1 >= String.length s then i+1 else process_trailing_aux (i+1) (i+n) in + (if j = i+n then + Buffer.add_string buff (String.sub s i n) + else + let v = Array.init (j-i) (fun k -> mk_escape (Char.code s.[i+k])) in + Buffer.add_string buff (String.concat "" (Array.to_list v))); + j in + let rec process i = + if i >= String.length s then Buffer.contents buff else + let c = String.unsafe_get s i in + match c with + | '\000'..'\127' -> Buffer.add_char buff c; process (i+1) + | '\128'..'\191' | '\248'..'\255' -> Buffer.add_string buff (mk_escape (Char.code c)); process (i+1) + | '\192'..'\223' -> process (process_trailing i 2) + | '\224'..'\239' -> process (process_trailing i 3) + | '\240'..'\247' -> process (process_trailing i 4) + in + process 0 + +let escaped_if_non_utf8 s = + if is_utf8 s then s else escaped_non_utf8 s + (* Check the well-formedness of an identifier *) +let is_valid_ident_initial = function + | Letter | IdentSep -> true + | IdentPart | Symbol | Unknown -> false + let initial_refutation j n s = - match classify n with - | Letter -> None - | _ -> + if is_valid_ident_initial (classify n) then None + else let c = String.sub s 0 j in Some (false, "Invalid character '"^c^"' at beginning of identifier \""^s^"\".") +let is_valid_ident_trailing = function + | Letter | IdentSep | IdentPart -> true + | Symbol | Unknown -> false + let trailing_refutation i j n s = - match classify n with - | Letter | IdentPart -> None - | _ -> + if is_valid_ident_trailing (classify n) then None + else let c = String.sub s i j in Some (false, "Invalid character '"^c^"' in identifier \""^s^"\".") +let is_unknown = function + | Unknown -> true + | Letter | IdentSep | IdentPart | Symbol -> false + +let is_ident_part = function + | IdentPart -> true + | Letter | IdentSep | Symbol | Unknown -> false + +let is_ident_sep = function + | IdentSep -> true + | Letter | IdentPart | Symbol | Unknown -> false + let ident_refutation s = if s = ".." then None else try let j, n = next_utf8 s 0 in @@ -198,7 +252,7 @@ let ident_refutation s = |x -> x with | End_of_input -> Some (true,"The empty string is not an identifier.") - | Invalid_argument _ -> Some (true,s^": invalid utf8 sequence.") + | Invalid_argument _ -> Some (true,escaped_non_utf8 s^": invalid utf8 sequence.") let lowercase_unicode = let tree = Segmenttree.make Unicodetable.to_lower in @@ -214,6 +268,26 @@ let lowercase_first_char s = let j, n = next_utf8 s 0 in utf8_of_unicode (lowercase_unicode n) +let split_at_first_letter s = + let n, v = next_utf8 s 0 in + if ((* optim *) n = 1 && s.[0] != '_') || not (is_ident_sep (classify v)) then None + else begin + let n = ref n in + let p = ref 0 in + while !n < String.length s && + let n', v = next_utf8 s !n in + p := n'; + (* Test if not letter *) + ((* optim *) n' = 1 && (s.[!n] = '_' || s.[!n] = '\'')) + || let st = classify v in + is_ident_sep st || is_ident_part st + do n := !n + !p + done; + let s1 = String.sub s 0 !n in + let s2 = String.sub s !n (String.length s - !n) in + Some (s1,s2) + end + (** For extraction, we need to encode unicode character into ascii ones *) let is_basic_ascii s = @@ -268,9 +342,7 @@ let utf8_length s = | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) - | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) - | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) - | '\254'..'\255' -> nc := 0 (* invalid byte *) + | '\248'..'\255' -> nc := 0 (* invalid byte *) end ; incr p ; while !p < len && !nc > 0 do @@ -299,9 +371,7 @@ let utf8_sub s start_u len_u = | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) - | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) - | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) - | '\254'..'\255' -> nc := 0 (* invalid byte *) + | '\248'..'\255' -> nc := 0 (* invalid byte *) end ; incr p ; while !p < len_b && !nc > 0 do diff --git a/lib/unicode.mli b/lib/unicode.mli index c7d7424801..32ffbb8e94 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -8,7 +8,7 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol | Unknown +type status (** Classify a unicode char into 3 classes or unknown. *) val classify : int -> status @@ -17,10 +17,23 @@ val classify : int -> status Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. *) val ident_refutation : string -> (bool * string) option +(** Tells if a valid initial character for an identifier *) +val is_valid_ident_initial : status -> bool + +(** Tells if a valid non-initial character for an identifier *) +val is_valid_ident_trailing : status -> bool + +(** Tells if a character is unclassified *) +val is_unknown : status -> bool + (** First char of a string, converted to lowercase @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string +(** Split a string supposed to be an ident at the first letter; + as an optimization, return None if the first character is a letter *) +val split_at_first_letter : string -> (string * string) option + (** Return [true] if all UTF-8 characters in the input string are just plain ASCII characters. Returns [false] otherwise. *) val is_basic_ascii : string -> bool @@ -40,3 +53,6 @@ val utf8_length : string -> int (** Variant of {!String.sub} for UTF-8 strings. *) val utf8_sub : string -> int -> int -> string + +(** Return a "%XX"-escaped string if it contains non UTF-8 characters. *) +val escaped_if_non_utf8 : string -> string diff --git a/library/library.ml b/library/library.ml index 28afa054e9..1da2c591d5 100644 --- a/library/library.ml +++ b/library/library.ml @@ -620,25 +620,6 @@ let check_coq_overwriting p id = (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") -(* Verifies that a string starts by a letter and do not contain - others caracters than letters, digits, or `_` *) - -let check_module_name s = - let msg c = - strbrk "Invalid module name: " ++ str s ++ strbrk " character " ++ - (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++ - strbrk " is not allowed in module names\n" - in - let err c = user_err (msg c) in - match String.get s 0 with - | 'a' .. 'z' | 'A' .. 'Z' -> - for i = 1 to (String.length s)-1 do - match String.get s i with - | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> () - | c -> err c - done - | c -> err c - let start_library fo = let ldir0 = try @@ -648,7 +629,6 @@ let start_library fo = in let file = Filename.chop_extension (Filename.basename fo) in let id = Id.of_string file in - check_module_name file; check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 9c9189ffeb..f26398fa92 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -245,8 +245,8 @@ let check_ident str = loop_id true s | [< s >] -> match unlocated lookup_utf8 Ploc.dummy s with - | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s - | Utf8Token (Unicode.IdentPart, n) when intail -> + | Utf8Token (st, n) when not intail && Unicode.is_valid_ident_initial st -> njunk n s; loop_id true s + | Utf8Token (st, n) when intail && Unicode.is_valid_ident_trailing st -> njunk n s; loop_id true s | EmptyStream -> () @@ -311,9 +311,9 @@ let rec ident_tail loc len = parser ident_tail loc (store len c) s | [< s >] -> match lookup_utf8 loc s with - | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) -> + | Utf8Token (st, n) when Unicode.is_valid_ident_trailing st -> ident_tail loc (nstore n len s) s - | Utf8Token (Unicode.Unknown, n) -> + | Utf8Token (st, n) when Unicode.is_unknown st -> let id = get_buff len in let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in warn_unrecognized_unicode ~loc:!@loc (u,id); len @@ -539,7 +539,7 @@ let parse_after_dot loc c bp = (try find_keyword loc ("."^field) s with Not_found -> FIELD field) | [< s >] -> match lookup_utf8 loc s with - | Utf8Token (Unicode.Letter, n) -> + | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in let field = get_buff len in (try find_keyword loc ("."^field) s with Not_found -> FIELD field) @@ -553,7 +553,7 @@ let parse_after_qmark loc bp s = | None -> KEYWORD "?" | _ -> match lookup_utf8 loc s with - | Utf8Token (Unicode.Letter, _) -> LEFTQMARK + | Utf8Token (st, _) when Unicode.is_valid_ident_initial st -> LEFTQMARK | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp '?' s) @@ -618,13 +618,13 @@ let rec next_token loc = parser bp comment_stop bp; between_commands := new_between_commands; t | [< s >] -> match lookup_utf8 loc s with - | Utf8Token (Unicode.Letter, n) -> + | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in let id = get_buff len in let ep = Stream.count s in comment_stop bp; (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep - | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) -> + | AsciiChar | Utf8Token _ -> let t = process_chars loc bp (Stream.next s) s in comment_stop bp; t | EmptyStream -> diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index f503c572d0..3c46d5c43b 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -342,7 +342,7 @@ let rec extract_structure env mp reso ~all = function and extract_mexpr env mp = function | MEwith _ -> assert false (* no 'with' syntax for modules *) - | me when lang () != Ocaml -> + | me when lang () != Ocaml || Table.is_extrcompute () -> (* In Haskell/Scheme, we expand everything. For now, we also extract everything, dead code will be removed later (see [Modutil.optimize_struct]. *) @@ -570,11 +570,12 @@ let print_structure_to_file (fn,si,mo) dry struc = let reset () = Visit.reset (); reset_tables (); reset_renaming_tables Everything -let init modular library = +let init ?(compute=false) modular library = check_inside_section (); check_inside_module (); set_keywords (descr ()).keywords; set_modular modular; set_library library; + set_extrcompute compute; reset (); if modular && lang () == Scheme then error_scheme () @@ -684,8 +685,22 @@ let extraction_library is_rec m = List.iter print struc; reset () +(** For extraction compute, we flatten all the module structure, + getting rid of module types or unapplied functors *) + +let flatten_structure struc = + let rec flatten_elem (lab,elem) = match elem with + |SEdecl d -> [d] + |SEmodtype _ -> [] + |SEmodule m -> match m.ml_mod_expr with + |MEfunctor _ -> [] + |MEident _ | MEapply _ -> assert false (* should be expanded *) + |MEstruct (_,elems) -> flatten_elems elems + and flatten_elems l = List.flatten (List.map flatten_elem l) + in flatten_elems (List.flatten (List.map snd struc)) + let structure_for_compute c = - init false false; + init false false ~compute:true; let env = Global.env () in let ast, mlt = Extraction.extract_constr env c in let ast = Mlutil.normalize ast in @@ -694,8 +709,7 @@ let structure_for_compute c = let () = ast_iter_references add_ref add_ref add_ref ast in let refs = Refset.elements !refs in let struc = optimize_struct (refs,[]) (mono_environment refs []) in - let flatstruc = List.map snd (List.flatten (List.map snd struc)) in - flatstruc, ast, mlt + (flatten_structure struc), ast, mlt (* For the test-suite : extraction to a temporary file + run ocamlc on it *) diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 5769ff1176..7bbb825b10 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -34,5 +34,4 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Term.constr -> - Miniml.ml_flat_structure * Miniml.ml_ast * Miniml.ml_type + Term.constr -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index edebba49df..5e967ef379 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -187,8 +187,6 @@ type ml_structure = (ModPath.t * ml_module_structure) list type ml_signature = (ModPath.t * ml_module_sig) list -type ml_flat_structure = ml_structure_elem list - type unsafe_needs = { mldummy : bool; tdummy : bool; diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a4c2bcd883..b01b0198d5 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -127,11 +127,15 @@ let rec mgu = function | Taxiom, Taxiom -> () | _ -> raise Impossible -let needs_magic p = try mgu p; false with Impossible -> true +let skip_typing () = lang () == Scheme || is_extrcompute () -let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a +let needs_magic p = + if skip_typing () then false + else try mgu p; false with Impossible -> true -let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a +let put_magic_if b a = if b then MLmagic a else a + +let put_magic p a = if needs_magic p then MLmagic a else a let generalizable a = lang () != Ocaml || @@ -769,6 +773,20 @@ let eta_red e = else e | _ -> e +(* Performs an eta-reduction when the core is atomic, + or otherwise returns None *) + +let atomic_eta_red e = + let ids,t = collect_lams e in + let n = List.length ids in + match t with + | MLapp (f,a) when test_eta_args_lift 0 n a -> + (match f with + | MLrel k when k>n -> Some (MLrel (k-n)) + | MLglob _ | MLexn _ | MLdummy _ -> Some f + | _ -> None) + | _ -> None + (*s Computes all head linear beta-reductions possible in [(t a)]. Non-linear head beta-redex become let-in. *) @@ -1053,6 +1071,10 @@ let rec simpl o = function simpl o (MLcase(typ,e,br')) | MLmagic(MLdummy _ as e) when lang () == Haskell -> e | MLmagic(MLexn _ as e) -> e + | MLlam _ as e -> + (match atomic_eta_red e with + | Some e' -> e' + | None -> ast_map (simpl o) e) | a -> ast_map (simpl o) a (* invariant : list [a] of arguments is non-empty *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 30e3b520f9..995d5fd19d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -250,6 +250,11 @@ let modular () = !modular_ref let set_library b = library_ref := b let library () = !library_ref +let extrcompute = ref false + +let set_extrcompute b = extrcompute := b +let is_extrcompute () = !extrcompute + (*s Printing. *) (* The following functions work even on objects not in [Global.env ()]. diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 7e47d0bc81..cc93f294b3 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -165,6 +165,9 @@ val modular : unit -> bool val set_library : bool -> unit val library : unit -> bool +val set_extrcompute : bool -> unit +val is_extrcompute : unit -> bool + (*s Table for custom inlining *) val to_inline : global_reference -> bool diff --git a/test-suite/Makefile b/test-suite/Makefile index ae426f0daf..61e75fa5d3 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -92,7 +92,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ coqdoc # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log @@ -156,6 +156,7 @@ summary: $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ + $(call summary_dir, "Coqwc tests", coqwc); \ $(call summary_dir, "Coq makefile", coq-makefile); \ $(call summary_dir, "Coqdoc tests", coqdoc); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ @@ -498,6 +499,26 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) fi; \ } > "$@" +# coqwc : test output + +coqwc : $(patsubst %.v,%.v.log,$(wildcard coqwc/*.v)) + +coqwc/%.v.log : coqwc/%.v + $(HIDE){ \ + echo $(call log_intro,$<); \ + tmpoutput=`mktemp /tmp/coqwc.XXXXXX`; \ + $(BIN)coqwc $< 2>&1 > $$tmpoutput; \ + diff -u --strip-trailing-cr coqwc/$*.out $$tmpoutput 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + fi; \ + rm $$tmpoutput; \ + } > "$@" + # coq_makefile coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) diff --git a/test-suite/bugs/closed/4852.v b/test-suite/bugs/closed/4852.v new file mode 100644 index 0000000000..5068ed9b95 --- /dev/null +++ b/test-suite/bugs/closed/4852.v @@ -0,0 +1,54 @@ +(** BZ 4852 : unsatisfactory Extraction Implicit for a fixpoint defined via wf *) + +Require Import Coq.Lists.List. +Import ListNotations. +Require Import Omega. + +Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf. + +Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) := + let R := fresh in + let E := fresh in + remember term as R eqn:E; + revert E; revert Hs; + induction R as [R H] using wfi_lt; + intros; subst R. + +Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws. + +Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega. + +Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'"). + +Definition split_acc (ls : list nat) : forall acc1 acc2, + (|acc1| = |acc2| \/ |acc1| = S (|acc2|)) -> + { lss : list nat * list nat | + let '(ls1, ls2) := lss in |ls1++ls2| = |ls++acc1++acc2| /\ (|ls1| = |ls2| \/ |ls1| = S (|ls2|))}. +Proof. + induction ls as [|a ls IHls]. all:intros acc1 acc2 H. + { exists (acc1, acc2). cbn. intuition reflexivity. } + destruct (IHls (a::acc2) acc1) as [[ls1 ls2] (H1 & H2)]. 1:solve_nat. + exists (ls1, ls2). cbn. intuition solve_nat. +Defined. + +Definition join(ls : list nat) : { rls : list nat | |rls| = |ls| }. +Proof. + wfinduction (|ls|) on ls as IH. + case (split_acc ls [] []). 1:solve_nat. + intros (ls1 & ls2) (H1 & H2). + destruct ls2 as [|a ls2]. + - exists ls1. solve_nat. + - unshelve eelim (IH _ _ ls1 eq_refl). 1:solve_nat. intros rls1 H3. + unshelve eelim (IH _ _ ls2 eq_refl). 1:solve_nat. intros rls2 H4. + exists (a :: rls1 ++ rls2). solve_nat. +Defined. + +Require Import ExtrOcamlNatInt. +Extract Inlined Constant length => "List.length". +Extract Inlined Constant app => "List.append". + +Extraction Inline wfi_lt. +Extraction Implicit wfi_lt [1 3]. +Recursive Extraction join. (* was: Error: An implicit occurs after extraction *) +Extraction TestCompile join. + diff --git a/test-suite/bugs/closed/5757.v b/test-suite/bugs/closed/5757.v new file mode 100644 index 0000000000..0d0f2eed44 --- /dev/null +++ b/test-suite/bugs/closed/5757.v @@ -0,0 +1,76 @@ +(* Check that resolved status of evars follows "restrict" *) + +Axiom H : forall (v : nat), Some 0 = Some v -> True. +Lemma L : True. +eapply H with _; +match goal with + | |- Some 0 = Some ?v => change (Some (0+0) = Some v) +end. +Abort. + +(* The original example *) + +Set Default Proof Using "Type". + +Module heap_lang. + +Inductive expr := + | InjR (e : expr). + +Inductive val := + | InjRV (v : val). + +Bind Scope val_scope with val. + +Fixpoint of_val (v : val) : expr := + match v with + | InjRV v => InjR (of_val v) + end. + +Fixpoint to_val (e : expr) : option val := None. + +End heap_lang. +Export heap_lang. + +Module W. +Inductive expr := + | Val (v : val) + (* Sums *) + | InjR (e : expr). + +Fixpoint to_expr (e : expr) : heap_lang.expr := + match e with + | Val v => of_val v + | InjR e => heap_lang.InjR (to_expr e) + end. + +End W. + + + +Section Tests. + + Context (iProp: Type). + Context (WPre: expr -> Prop). + + Context (tac_wp_alloc : + forall (e : expr) (v : val), + to_val e = Some v -> WPre e). + + Lemma push_atomic_spec (x: val) : + WPre (InjR (of_val x)). + Proof. +(* This works. *) +eapply tac_wp_alloc with _. +match goal with + | |- to_val ?e = Some ?v => + change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v) +end. +Undo. Undo. +(* This is fixed *) +eapply tac_wp_alloc with _; +match goal with + | |- to_val ?e = Some ?v => + change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v) +end. +Abort. diff --git a/test-suite/bugs/closed/5765.v b/test-suite/bugs/closed/5765.v new file mode 100644 index 0000000000..343ab49357 --- /dev/null +++ b/test-suite/bugs/closed/5765.v @@ -0,0 +1,3 @@ +(* 'pat binder not (yet?) allowed in parameters of inductive types *) + +Fail Inductive X '(a,b) := x. diff --git a/test-suite/bugs/closed/5769.v b/test-suite/bugs/closed/5769.v new file mode 100644 index 0000000000..42573aad87 --- /dev/null +++ b/test-suite/bugs/closed/5769.v @@ -0,0 +1,20 @@ +(* Check a few naming heuristics based on types *) +(* was buggy for types names _something *) + +Inductive _foo :=. +Lemma bob : (sigT (fun x : nat => _foo)) -> _foo. +destruct 1. +exact _f. +Abort. + +Inductive _'Foo :=. +Lemma bob : (sigT (fun x : nat => _'Foo)) -> _'Foo. +destruct 1. +exact _'f. +Abort. + +Inductive ____ :=. +Lemma bob : (sigT (fun x : nat => ____)) -> ____. +destruct 1. +exact x0. +Abort. diff --git a/test-suite/coqwc/BZ5637.out b/test-suite/coqwc/BZ5637.out new file mode 100644 index 0000000000..f0b5e4f7eb --- /dev/null +++ b/test-suite/coqwc/BZ5637.out @@ -0,0 +1,2 @@ + spec proof comments + 5 0 0 coqwc/BZ5637.v diff --git a/test-suite/coqwc/BZ5637.v b/test-suite/coqwc/BZ5637.v new file mode 100644 index 0000000000..6428b10ff8 --- /dev/null +++ b/test-suite/coqwc/BZ5637.v @@ -0,0 +1,5 @@ +Local Obligation Tactic := idtac. +Definition a := 1. +Definition b := 1. +Definition c := 1. +Definition d := 1. diff --git a/test-suite/coqwc/BZ5756.out b/test-suite/coqwc/BZ5756.out new file mode 100644 index 0000000000..039d1e5008 --- /dev/null +++ b/test-suite/coqwc/BZ5756.out @@ -0,0 +1,2 @@ + spec proof comments + 3 0 2 coqwc/BZ5756.v diff --git a/test-suite/coqwc/BZ5756.v b/test-suite/coqwc/BZ5756.v new file mode 100644 index 0000000000..ccb12076a3 --- /dev/null +++ b/test-suite/coqwc/BZ5756.v @@ -0,0 +1,3 @@ +Definition myNextValue := 0. (* OK *) +Definition x := myNextValue. (* not OK *) +Definition y := 0. diff --git a/test-suite/coqwc/false.out b/test-suite/coqwc/false.out new file mode 100644 index 0000000000..14c5713f6d --- /dev/null +++ b/test-suite/coqwc/false.out @@ -0,0 +1,2 @@ + spec proof comments + 3 3 1 coqwc/false.v diff --git a/test-suite/coqwc/false.v b/test-suite/coqwc/false.v new file mode 100644 index 0000000000..640f9ea7f0 --- /dev/null +++ b/test-suite/coqwc/false.v @@ -0,0 +1,8 @@ +Axiom x : nat. + +Definition foo (x : nat) := x + 1. + +Lemma bar : False. + idtac. + idtac. (* truth is overrated *) +Admitted. diff --git a/test-suite/coqwc/next-obligation.out b/test-suite/coqwc/next-obligation.out new file mode 100644 index 0000000000..7a0fd777c1 --- /dev/null +++ b/test-suite/coqwc/next-obligation.out @@ -0,0 +1,2 @@ + spec proof comments + 1 7 0 coqwc/next-obligation.v diff --git a/test-suite/coqwc/next-obligation.v b/test-suite/coqwc/next-obligation.v new file mode 100644 index 0000000000..786df98913 --- /dev/null +++ b/test-suite/coqwc/next-obligation.v @@ -0,0 +1,10 @@ +(* make sure all proof lines are counted *) + +Goal True. + Next Obligation. + idtac. + Next Obligation. + idtac. + Next Obligation. + idtac. +Qed. diff --git a/test-suite/coqwc/theorem.out b/test-suite/coqwc/theorem.out new file mode 100644 index 0000000000..d01507bf78 --- /dev/null +++ b/test-suite/coqwc/theorem.out @@ -0,0 +1,2 @@ + spec proof comments + 1 9 2 coqwc/theorem.v diff --git a/test-suite/coqwc/theorem.v b/test-suite/coqwc/theorem.v new file mode 100644 index 0000000000..901c9074fd --- /dev/null +++ b/test-suite/coqwc/theorem.v @@ -0,0 +1,10 @@ +Theorem foo : True. +Proof. + idtac. (* comment *) + idtac. + idtac. + idtac. (* comment *) + idtac. + idtac. + auto. +Qed. diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh new file mode 100755 index 0000000000..13e264c09c --- /dev/null +++ b/test-suite/misc/deps-utf8.sh @@ -0,0 +1,17 @@ +# Check reading directories matching non pure ascii idents +# See bug #5715 (utf-8 working on macos X and linux) +# Windows is still not compliant +a=`uname` +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +rm -f misc/deps/théorèmes/*.v +tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` +$coqc -R misc/deps AlphaBêta misc/deps/αβ/γδ.v +R=$? +$coqtop -R misc/deps AlphaBêta -load-vernac-source misc/deps/αβ/εζ.v +S=$? +if [ $R = 0 -a $S = 0 ]; then + exit 0 +else + exit 1 +fi +fi diff --git a/test-suite/misc/deps/αβ/γδ.v b/test-suite/misc/deps/αβ/γδ.v new file mode 100644 index 0000000000..f43a2d6571 --- /dev/null +++ b/test-suite/misc/deps/αβ/γδ.v @@ -0,0 +1,4 @@ +Theorem simple : forall A, A -> A. +Proof. +auto. +Qed. diff --git a/test-suite/misc/deps/αβ/εζ.v b/test-suite/misc/deps/αβ/εζ.v new file mode 100644 index 0000000000..e7fd25c0d1 --- /dev/null +++ b/test-suite/misc/deps/αβ/εζ.v @@ -0,0 +1 @@ +Require Import γδ. diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v index 672222bdd6..a4fa544cd9 100644 --- a/test-suite/success/unshelve.v +++ b/test-suite/success/unshelve.v @@ -9,3 +9,11 @@ unshelve (refine (F _ _ _ _)). + exact (@eq_refl bool true). + exact (@eq_refl unit tt). Qed. + +(* This was failing in 8.6, because of ?a:nat being wrongly duplicated *) + +Goal (forall a : nat, a = 0 -> True) -> True. +intros F. +unshelve (eapply (F _);clear F). +2:reflexivity. +Qed. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index afe8e62ee3..cfa5526025 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -39,6 +39,7 @@ CAMLP4O := $(COQMF_CAMLP4O) CAMLP4BIN := $(COQMF_CAMLP4BIN) CAMLP4LIB := $(COQMF_CAMLP4LIB) CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) +CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @CONF_FILE@: @PROJECT_FILE@ @@ -100,11 +101,11 @@ AFTER ?= CAMLDONTLINK=camlp5.gramlib,unix,str # OCaml binaries -CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread -CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK) -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK) -CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -rectypes +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack # DESTDIR is prepended to all installation paths @@ -114,8 +115,6 @@ DESTDIR ?= CAMLDEBUG ?= COQDEBUG ?= -# Extra flags to the OCaml compiler -CAMLFLAGS ?= # Extra packages to be linked in (as in findlib -package) CAMLPKGS ?= @@ -749,7 +748,7 @@ printenv:: # file you can extend the merlin-hook target in @LOCAL_FILE@ .merlin: $(SHOW)'FILL .merlin' - $(HIDE)echo 'FLG -rectypes -thread' > .merlin + $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin $(HIDE)echo 'B $(COQLIB)' >> .merlin $(HIDE)echo 'S $(COQLIB)' >> .merlin $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 8eeb59898f..564e20d0e8 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -25,8 +25,6 @@ exception Fin_fichier exception Syntax_error of int*int - let field_name s = String.sub s 1 (String.length s - 1) - let unquote_string s = String.sub s 1 (String.length s - 2) @@ -40,6 +38,18 @@ let syntax_error lexbuf = raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf)) + let check_valid lexbuf s = + match Unicode.ident_refutation s with + | None -> s + | Some _ -> syntax_error lexbuf + + let get_ident lexbuf = + let s = Lexing.lexeme lexbuf in check_valid lexbuf s + + let get_field_name lexbuf = + let s = Lexing.lexeme lexbuf in + check_valid lexbuf (String.sub s 1 (String.length s - 1)) + [@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *) let uncapitalize = String.uncapitalize [@@@ocaml.warning "+3"] @@ -52,20 +62,8 @@ let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9'] let caml_up_ident = uppercase identchar* let caml_low_ident = lowercase identchar* -let coq_firstchar = - (* This is only an approximation, refer to lib/util.ml for correct def *) - ['A'-'Z' 'a'-'z' '_'] | - (* superscript 1 *) - '\194' '\185' | - (* utf-8 latin 1 supplement *) - '\195' ['\128'-'\150'] | '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] | - (* utf-8 letters *) - '\206' (['\145'-'\161'] | ['\163'-'\187']) - '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) - | '\129' [ '\176'-'\187' ] (* superscripts *) - | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) -let coq_identchar = coq_firstchar | ['\'' '0'-'9'] -let coq_ident = coq_firstchar coq_identchar* +(* This is an overapproximation, we check correctness afterwards *) +let coq_ident = ['A'-'Z' 'a'-'z' '_' '\128'-'\255'] ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9' '\128'-'\255']* let coq_field = '.' coq_ident let dot = '.' ( space+ | eof) @@ -102,7 +100,7 @@ and from_rule = parse | space+ { from_rule lexbuf } | coq_ident - { let from = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in + { let from = coq_qual_id_tail [get_ident lexbuf] lexbuf in consume_require (Some from) lexbuf } | eof { syntax_error lexbuf } @@ -241,7 +239,7 @@ and load_file = parse parse_dot lexbuf; Load (unquote_vfile_string s) } | coq_ident - { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s } + { let s = get_ident lexbuf in skip_to_dot lexbuf; Load s } | eof { syntax_error lexbuf } | _ @@ -253,7 +251,7 @@ and require_file from = parse | space+ { require_file from lexbuf } | coq_ident - { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in + { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in let qid = coq_qual_id_list [name] lexbuf in parse_dot lexbuf; Require (from, qid) } @@ -278,7 +276,7 @@ and coq_qual_id = parse | space+ { coq_qual_id lexbuf } | coq_ident - { coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf } + { coq_qual_id_tail [get_ident lexbuf] lexbuf } | _ { syntax_error lexbuf } @@ -288,7 +286,7 @@ and coq_qual_id_tail module_name = parse | space+ { coq_qual_id_tail module_name lexbuf } | coq_field - { coq_qual_id_tail (field_name (Lexing.lexeme lexbuf) :: module_name) lexbuf } + { coq_qual_id_tail (get_field_name lexbuf :: module_name) lexbuf } | eof { syntax_error lexbuf } | _ @@ -301,7 +299,7 @@ and coq_qual_id_list module_names = parse | space+ { coq_qual_id_list module_names lexbuf } | coq_ident - { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in + { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in coq_qual_id_list (name :: module_names) lexbuf } | eof diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 28a3c791cb..c21db300ad 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -252,6 +252,17 @@ let create_tmp_main_file modules = with reraise -> clean main_name; raise reraise +(* TODO: remove once OCaml 4.04 is adopted *) +let split_on_char sep s = + let r = ref [] in + let j = ref (String.length s) in + for i = String.length s - 1 downto 0 do + if s.[i] = sep then begin + r := String.sub s (i + 1) (!j - i - 1) :: !r; + j := i + end + done; + String.sub s 0 !j :: !r (** {6 Main } *) @@ -271,8 +282,10 @@ let main () = try (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper. - With the coq .cma, we MUST use the -linkall option. *) + let coq_camlflags = + List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in let args = - "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @ + coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @ (std_includes basedir) @ tolink @ [ main_file ] @ topstart in if !echo then begin diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c1cdaa5a34..db7bcb76b1 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -539,7 +539,12 @@ let parse_args arglist = |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo |"-toploop" -> set_toploop (next ()) - |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ())) + |"-w" | "-W" -> + let w = next () in + if w = "none" then CWarnings.set_flags w + else + let w = CWarnings.get_flags () ^ "," ^ w in + CWarnings.set_flags (CWarnings.normalize_flags_string w) |"-o" -> Flags.compilation_output_name := Some (next()) (* Options with zero arg *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b0f021cdcd..1b020bc876 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -47,35 +47,29 @@ let beautify_suffix = ".beautified" let set_formatter_translator ch = let out s b e = output_substring ch s b e in - Format.set_formatter_output_functions out (fun () -> flush ch); - Format.set_max_boxes max_int + let ft = Format.make_formatter out (fun () -> flush ch) in + Format.pp_set_max_boxes ft max_int; + ft -let pr_new_syntax_in_context ?loc chan_beautify ocom = +let pr_new_syntax_in_context ?loc ft_beautify ocom = let loc = Option.cata Loc.unloc (0,0) loc in - if !Flags.beautify_file then set_formatter_translator chan_beautify; let fs = States.freeze ~marshallable:`No in - (* The content of this is not supposed to fail, but if ever *) - try - (* Side-effect: order matters *) - let before = comment (CLexer.extract_comments (fst loc)) in - let com = match ocom with - | Some com -> Ppvernac.pr_vernac com - | None -> mt() in - let after = comment (CLexer.extract_comments (snd loc)) in - if !Flags.beautify_file then - (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after)); - Format.pp_print_flush !Topfmt.std_ft ()) - else - Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); - States.unfreeze fs; - Format.set_formatter_out_channel stdout - with any -> - States.unfreeze fs; - Format.set_formatter_out_channel stdout - -let pr_new_syntax ?loc po chan_beautify ocom = + (* Side-effect: order matters *) + let before = comment (CLexer.extract_comments (fst loc)) in + let com = match ocom with + | Some com -> Ppvernac.pr_vernac com + | None -> mt() in + let after = comment (CLexer.extract_comments (snd loc)) in + if !Flags.beautify_file then + (Pp.pp_with ft_beautify (hov 0 (before ++ com ++ after)); + Format.pp_print_flush ft_beautify ()) + else + Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); + States.unfreeze fs + +let pr_new_syntax ?loc po ft_beautify ocom = (* Reinstall the context of parsing which includes the bindings of comments to locations *) - Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc chan_beautify) ocom + Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc ft_beautify) ocom (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) @@ -183,8 +177,13 @@ let rec interp_vernac sid (loc,com) = (* Load a vernac file. CErrors are annotated with file and location *) and load_vernac verbosely sid file = - let chan_beautify = - if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in + let ft_beautify, close_beautify = + if !Flags.beautify_file then + let chan_beautify = open_out (file^beautify_suffix) in + set_formatter_translator chan_beautify, fun () -> close_out chan_beautify; + else + !Topfmt.std_ft, fun () -> () + in let in_chan = open_utf8_file_in file in let in_echo = if verbosely then Some (open_utf8_file_in file) else None in let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in @@ -214,7 +213,7 @@ and load_vernac verbosely sid file = *) in (* Printing of vernacs *) - if !Flags.beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast); + if !Flags.beautify then pr_new_syntax ?loc in_pa ft_beautify (Some ast); Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); @@ -230,11 +229,11 @@ and load_vernac verbosely sid file = | Stm.End_of_input -> (* Is this called so comments at EOF are printed? *) if !Flags.beautify then - pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None; - if !Flags.beautify_file then close_out chan_beautify; + pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None; + if !Flags.beautify_file then close_beautify (); !rsid | reraise -> - if !Flags.beautify_file then close_out chan_beautify; + if !Flags.beautify_file then close_beautify (); iraise (disable_drop e, info) (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit] diff --git a/vernac/command.ml b/vernac/command.ml index 120f9590f2..a1a87d54e0 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -518,7 +518,8 @@ let check_param = function | CLocalDef (na, _, _) -> check_named na | CLocalAssum (nas, Default _, _) -> List.iter check_named nas | CLocalAssum (nas, Generalized _, _) -> () -| CLocalPattern _ -> assert false +| CLocalPattern (loc,_) -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = check_all_names_different indl; diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 12b68fe38e..189c47aab9 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -84,7 +84,7 @@ let rec contract3' env sigma a b c = function (** Ad-hoc reductions *) let j_nf_betaiotaevar sigma j = - { uj_val = Evarutil.nf_evar sigma j.uj_val; + { uj_val = j.uj_val; uj_type = Reductionops.nf_betaiota sigma j.uj_type } let jv_nf_betaiotaevar sigma jl = @@ -173,7 +173,6 @@ let explain_unbound_var env v = str "No such section variable or assumption: " ++ var ++ str "." let explain_not_type env sigma j = - let j = Evarutil.j_nf_evar sigma j in let pe = pr_ne_context_of (str "In environment") env sigma in let pc,pt = pr_ljudge_env env sigma j in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ @@ -241,7 +240,6 @@ let explain_elim_arity env sigma ind sorts c pj okinds = fnl () ++ msg let explain_case_not_inductive env sigma cj = - let cj = Evarutil.j_nf_evar sigma cj in let env = make_all_name_different env sigma in let pc = pr_leconstr_env env sigma cj.uj_val in let pct = pr_leconstr_env env sigma cj.uj_type in @@ -254,7 +252,6 @@ let explain_case_not_inductive env sigma cj = str "which is not a (co-)inductive type." let explain_number_branches env sigma cj expn = - let cj = Evarutil.j_nf_evar sigma cj in let env = make_all_name_different env sigma in let pc = pr_leconstr_env env sigma cj.uj_val in let pct = pr_leconstr_env env sigma cj.uj_type in @@ -263,7 +260,7 @@ let explain_number_branches env sigma cj expn = str "expects " ++ int expn ++ str " branches." let explain_ill_formed_branch env sigma c ci actty expty = - let simp t = Reductionops.nf_betaiota sigma (Evarutil.nf_evar sigma t) in + let simp t = Reductionops.nf_betaiota sigma t in let env = make_all_name_different env sigma in let pc = pr_leconstr_env env sigma c in let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in @@ -300,10 +297,10 @@ let explain_unification_error env sigma p1 p2 = function | NotSameArgSize | NotSameHead | NoCanonicalStructure -> (* Error speaks from itself *) [] | ConversionFailed (env,t1,t2) -> + let t1 = Reductionops.nf_betaiota sigma t1 in + let t2 = Reductionops.nf_betaiota sigma t2 in if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else let env = make_all_name_different env sigma in - let t1 = Evarutil.nf_evar sigma t1 in - let t2 = Evarutil.nf_evar sigma t2 in if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then let t1, t2 = pr_explicit env sigma t1 t2 in [str "cannot unify " ++ t1 ++ strbrk " and " ++ t2] @@ -327,8 +324,6 @@ let explain_unification_error env sigma p1 p2 = function | CannotSolveConstraint ((pb,env,t,u),e) -> let t = EConstr.of_constr t in let u = EConstr.of_constr u in - let t = Evarutil.nf_evar sigma t in - let u = Evarutil.nf_evar sigma u in let env = make_all_name_different env sigma in (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ str " == " ++ pr_leconstr_env env sigma u) @@ -359,9 +354,7 @@ let explain_actual_type env sigma j t reason = let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let randl = jv_nf_betaiotaevar sigma randl in - let exptyp = Evarutil.nf_evar sigma exptyp in let actualtyp = Reductionops.nf_betaiota sigma actualtyp in - let rator = Evarutil.j_nf_evar sigma rator in let env = make_all_name_different env sigma in let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in let nargs = Array.length randl in @@ -386,8 +379,6 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = exptyp ++ str "." let explain_cant_apply_not_functional env sigma rator randl = - let randl = Evarutil.jv_nf_evar sigma randl in - let rator = Evarutil.j_nf_evar sigma rator in let env = make_all_name_different env sigma in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env sigma in*) @@ -407,8 +398,6 @@ let explain_cant_apply_not_functional env sigma rator randl = fnl () ++ str " " ++ v 0 appl let explain_unexpected_type env sigma actual_type expected_type = - let actual_type = Evarutil.nf_evar sigma actual_type in - let expected_type = Evarutil.nf_evar sigma expected_type in let pract, prexp = pr_explicit env sigma actual_type expected_type in str "Found type" ++ spc () ++ pract ++ spc () ++ str "where" ++ spc () ++ prexp ++ str " was expected." @@ -510,8 +499,6 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = with e when CErrors.noncritical e -> mt ()) let explain_ill_typed_rec_body env sigma i names vdefj vargs = - let vdefj = Evarutil.jv_nf_evar sigma vdefj in - let vargs = Array.map (Evarutil.nf_evar sigma) vargs in let env = make_all_name_different env sigma in let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in @@ -575,9 +562,9 @@ let rec explain_evar_kind env sigma evk ty = function | Evar_kinds.SubEvar evk' -> let evi = Evd.find sigma evk' in let pc = match evi.evar_body with - | Evar_defined c -> pr_leconstr_env env sigma (Evarutil.nf_evar sigma (EConstr.of_constr c)) + | Evar_defined c -> pr_leconstr_env env sigma (EConstr.of_constr c) | Evar_empty -> assert false in - let ty' = Evarutil.nf_evar sigma (EConstr.of_constr evi.evar_concl) in + let ty' = EConstr.of_constr evi.evar_concl in pr_existential_key sigma evk ++ str " of type " ++ ty ++ str " in the partial instance " ++ pc ++ str " found for " ++ explain_evar_kind env sigma evk' @@ -628,8 +615,6 @@ let explain_wrong_case_info env (ind,u) ci = let explain_cannot_unify env sigma m n e = let env = make_all_name_different env sigma in - let m = Evarutil.nf_evar sigma m in - let n = Evarutil.nf_evar sigma n in let pm, pn = pr_explicit env sigma m n in let ppreason = explain_unification_error env sigma m n e in let pe = pr_ne_context_of (str "In environment") env sigma in diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 1edbd1a850..d3de10235f 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -174,6 +174,7 @@ let warn_cannot_use_directory = let convert_string d = try Names.Id.of_string d with UserError _ -> + let d = Unicode.escaped_if_non_utf8 d in warn_cannot_use_directory d; raise Exit |