From d0bb369ff3a56749b6f980e6c4f73c4ab4232b4e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 24 Jun 2015 14:03:03 +0200 Subject: Less closures makes the GC happy. We lambda-lift by hand the graph traversal functions in Univ to allocate less closures. --- kernel/univ.ml | 72 ++++++++++++++++++++++++++++++---------------------------- 1 file changed, 37 insertions(+), 35 deletions(-) diff --git a/kernel/univ.ml b/kernel/univ.ml index 4af7fe7c1c..fce9e28d36 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -925,25 +925,7 @@ let fast_compare_neq strict g arcu arcv = if arc_is_lt arc then cmp c to_revert lt_todo le_todo else - let rec find lt_todo lt le = match le with - | [] -> - begin match lt with - | [] -> - let () = arc.status <- SetLt in - cmp c (arc :: to_revert) lt_todo le_todo - | u :: lt -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else find (arc :: lt_todo) lt le - end - | u :: le -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else find (arc :: lt_todo) lt le - in - find lt_todo arc.lt arc.le + process_lt c to_revert lt_todo le_todo arc arc.lt arc.le | [], arc::le_todo -> if arc == arcv then (* No need to continue inspecting universes above arc: @@ -955,23 +937,43 @@ let fast_compare_neq strict g arcu arcv = if arc_is_le arc then cmp c to_revert [] le_todo else - let rec find lt_todo lt = match lt with - | [] -> - let fold accu u = - let node = repr g u in - node :: accu - in - let le_new = List.fold_left fold le_todo arc.le in - let () = arc.status <- SetLe in - cmp c (arc :: to_revert) lt_todo le_new - | u :: lt -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else find (arc :: lt_todo) lt - in - find [] arc.lt + process_le c to_revert [] le_todo arc arc.lt + + and process_lt c to_revert lt_todo le_todo arc0 lt le = match le with + | [] -> + begin match lt with + | [] -> + let () = arc0.status <- SetLt in + cmp c (arc0 :: to_revert) lt_todo le_todo + | u :: lt -> + let arc = repr g u in + if arc == arcv then + if strict then (to_revert, FastLT) else (to_revert, FastLE) + else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le + end + | u :: le -> + let arc = repr g u in + if arc == arcv then + if strict then (to_revert, FastLT) else (to_revert, FastLE) + else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le + + and process_le c to_revert lt_todo le_todo arc0 lt = match lt with + | [] -> + let fold accu u = + let node = repr g u in + node :: accu + in + let le_new = List.fold_left fold le_todo arc0.le in + let () = arc0.status <- SetLe in + cmp c (arc0 :: to_revert) lt_todo le_new + | u :: lt -> + let arc = repr g u in + if arc == arcv then + if strict then (to_revert, FastLT) else (to_revert, FastLE) + else process_le c to_revert (arc :: lt_todo) le_todo arc0 lt + in + try let (to_revert, c) = cmp FastNLE [] [] [arcu] in (** Reset all the touched arcs. *) -- cgit v1.2.3 From 987117e3daba31cb669b563723c8af276380f5ab Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 24 Jun 2015 16:41:28 +0200 Subject: Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8. --- test-suite/output/Notations.out | 4 ++-- test-suite/output/inference.out | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 6efd671a8c..b1558dab1c 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -70,7 +70,7 @@ FST (0; 1) : Z Nil : forall A : Type, list A -NIL:list nat +NIL : list nat : list nat (false && I 3)%bool /\ I 6 : Prop @@ -78,7 +78,7 @@ NIL:list nat : Z * Z * Z * (Z * Z * Z) [|0 * (1, 2, 3); (4, 5, 6) * false|] : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) -fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z +fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z : (Z -> Z -> Z -> Z) -> Z Init.Nat.add : nat -> nat -> nat diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index b1952aecf5..f2d1447785 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,12 +6,12 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n in ?y ?y0:T n +fun n : nat => let x := A n in ?y ?y0 : T n : forall n : nat, T n where ?y : [n : nat x := A n : T n |- ?T0 -> T n] ?y0 : [n : nat x := A n : T n |- ?T0] -fun n : nat => ?y ?y0:T n +fun n : nat => ?y ?y0 : T n : forall n : nat, T n where ?y : [n : nat |- ?T0 -> T n] -- cgit v1.2.3 From 42893bd092c4a63174c97995b4fb561daf4de273 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 24 Jun 2015 16:45:01 +0200 Subject: More silent Makefile when looking for codesign. May still be wrong on Windows, though. --- Makefile.build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.build b/Makefile.build index 41220792d5..92c0d46f24 100644 --- a/Makefile.build +++ b/Makefile.build @@ -101,7 +101,7 @@ BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils -ifeq ($(shell which codesign > /dev/null && echo $(ARCH)),Darwin) +ifeq ($(shell which codesign 2>&1 > /dev/null && echo $(ARCH)),Darwin) LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist" CODESIGN:=codesign -s - else -- cgit v1.2.3 From 3d33b59d725760bee14668c744b057a75440012e Mon Sep 17 00:00:00 2001 From: Thomas Sibut-Pinote Date: Tue, 23 Jun 2015 14:49:01 +0200 Subject: Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly. This allows fatal_error to be used for printing anomalies at loading time. --- checker/check.mllib | 4 +- dev/printers.mllib | 4 +- grammar/grammar.mllib | 5 +- lib/clib.mllib | 1 + lib/errors.ml | 10 ++++ lib/errors.mli | 5 ++ lib/ppstyle.ml | 149 ++++++++++++++++++++++++++++++++++++++++++++++++ lib/ppstyle.mli | 70 +++++++++++++++++++++++ printing/ppstyle.ml | 149 ------------------------------------------------ printing/ppstyle.mli | 70 ----------------------- printing/printing.mllib | 1 - toplevel/coqtop.ml | 6 -- 12 files changed, 244 insertions(+), 230 deletions(-) create mode 100644 lib/ppstyle.ml create mode 100644 lib/ppstyle.mli delete mode 100644 printing/ppstyle.ml delete mode 100644 printing/ppstyle.mli diff --git a/checker/check.mllib b/checker/check.mllib index 22df375623..49ca6bf051 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,6 +1,7 @@ Coq_config Hook +Terminal Canary Hashset Hashcons @@ -23,13 +24,14 @@ Pp Segmenttree Unicodetable Unicode -Errors CObj CList CString CArray CStack Util +Ppstyle +Errors Ephemeron Future CUnix diff --git a/dev/printers.mllib b/dev/printers.mllib index 2f78c2e915..74f36f6f5a 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -27,13 +27,14 @@ Pp Segmenttree Unicodetable Unicode -Errors CObj CList CString CArray CStack Util +Ppstyle +Errors Bigint Dyn CUnix @@ -154,7 +155,6 @@ Tok Lexer Ppextend Pputils -Ppstyle Ppannotation Stdarg Constrarg diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 0b168377d9..60ea0df026 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,6 +1,7 @@ Coq_config Hook +Terminal Canary Hashset Hashcons @@ -19,12 +20,14 @@ Serialize Stateid Feedback Pp -Errors + CList CString CArray CStack Util +Ppstyle +Errors Bigint Predicate Segmenttree diff --git a/lib/clib.mllib b/lib/clib.mllib index 2da81c959f..7ff1d29359 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -29,6 +29,7 @@ Util Stateid Feedback Pp +Ppstyle Xml_lexer Xml_parser Xml_printer diff --git a/lib/errors.ml b/lib/errors.ml index c60442654a..c1d224dfcd 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -129,3 +129,13 @@ let handled e = let bottom _ = raise Bottom in try let _ = print_gen bottom !handle_stack e in true with Bottom -> false + +(** Prints info which is either an error or + an anomaly and then exits with the appropriate + error code *) + +let fatal_error info anomaly = + let msg = info ++ fnl () in + pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; + flush_all (); + exit (if anomaly then 129 else 1) diff --git a/lib/errors.mli b/lib/errors.mli index 8320ce409f..e5dad93fd0 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -92,3 +92,8 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool + +(** Prints info which is either an error or + an anomaly and then exits with the appropriate + error code *) +val fatal_error : Pp.std_ppcmds -> bool -> 'a diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml new file mode 100644 index 0000000000..fb334c706b --- /dev/null +++ b/lib/ppstyle.ml @@ -0,0 +1,149 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* assert false + +let set_style tag st = + try tags := String.Map.update tag st !tags with Not_found -> assert false + +let clear_styles () = + tags := String.Map.map (fun _ -> None) !tags + +let dump () = String.Map.bindings !tags + +let parse_config s = + let styles = Terminal.parse s in + let set accu (name, st) = + try String.Map.update name (Some st) accu with Not_found -> accu + in + tags := List.fold_left set !tags styles + +let tag = Pp.Tag.create "ppstyle" + +(** Default tag is to reset everything *) +let default = Terminal.({ + fg_color = Some `DEFAULT; + bg_color = Some `DEFAULT; + bold = Some false; + italic = Some false; + underline = Some false; + negative = Some false; +}) + +let empty = Terminal.make () + +let make_style_stack style_tags = + (** Not thread-safe. We should put a lock somewhere if we print from + different threads. Do we? *) + let style_stack = ref [] in + let peek () = match !style_stack with + | [] -> default (** Anomalous case, but for robustness *) + | st :: _ -> st + in + let push tag = + let style = + try + begin match String.Map.find tag style_tags with + | None -> empty + | Some st -> st + end + with Not_found -> empty + in + (** Use the merging of the latest tag and the one being currently pushed. + This may be useful if for instance the latest tag changes the background and + the current one the foreground, so that the two effects are additioned. *) + let style = Terminal.merge (peek ()) style in + let () = style_stack := style :: !style_stack in + Terminal.eval style + in + let pop _ = match !style_stack with + | [] -> + (** Something went wrong, we fallback *) + Terminal.eval default + | _ :: rem -> + let () = style_stack := rem in + Terminal.eval (peek ()) + in + let clear () = style_stack := [] in + push, pop, clear + +let error_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in + make ~style ["message"; "error"] + +let warning_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in + make ~style ["message"; "warning"] + +let debug_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in + make ~style ["message"; "debug"] + +let pp_tag t = match Pp.Tag.prj t tag with +| None -> "" +| Some key -> key + +let init_color_output () = + let push_tag, pop_tag, clear_tag = make_style_stack !tags in + let tag_handler = { + Format.mark_open_tag = push_tag; + Format.mark_close_tag = pop_tag; + Format.print_open_tag = ignore; + Format.print_close_tag = ignore; + } in + let open Pp_control in + let () = Format.pp_set_mark_tags !std_ft true in + let () = Format.pp_set_mark_tags !err_ft true in + let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in + let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in + let pptag = tag in + let open Pp in + let msg ?header ft strm = + let strm = match header with + | None -> hov 0 strm + | Some (h, t) -> + let tag = Pp.Tag.inj t pptag in + let h = Pp.tag tag (str h ++ str ":") in + hov 0 (h ++ spc () ++ strm) + in + pp_with ~pp_tag ft strm; + Format.pp_print_newline ft (); + Format.pp_print_flush ft (); + (** In case something went wrong, we reset the stack *) + clear_tag (); + in + let logger level strm = match level with + | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm + | Info -> msg !std_ft strm + | Notice -> msg !std_ft strm + | Warning -> + let header = ("Warning", warning_tag) in + Flags.if_warn (fun () -> msg ~header !err_ft strm) () + | Error -> msg ~header:("Error", error_tag) !err_ft strm + in + let () = set_logger logger in + () diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli new file mode 100644 index 0000000000..f5d6184cb1 --- /dev/null +++ b/lib/ppstyle.mli @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string list -> t +(** Create a new tag with the given name. Each name must be unique. The optional + style is taken as the default one. *) + +val repr : t -> string list +(** Gives back the original name of the style tag where each string has been + concatenated and separated with a dot. *) + +val tag : t Pp.Tag.key +(** An annotation for styles *) + +(** {5 Manipulating global styles} *) + +val get_style : t -> Terminal.style option +(** Get the style associated to a tag. *) + +val set_style : t -> Terminal.style option -> unit +(** Set a style associated to a tag. *) + +val clear_styles : unit -> unit +(** Clear all styles. *) + +val parse_config : string -> unit +(** Add all styles from the given string as parsed by {!Terminal.parse}. + Unregistered tags are ignored. *) + +val dump : unit -> (t * Terminal.style option) list +(** Recover the list of known tags together with their current style. *) + +(** {5 Setting color output} *) + +val init_color_output : unit -> unit +(** Once called, all tags defined here will use their current style when + printed. To this end, this function redefines the loggers used when sending + messages to the user. The program will in particular use the formatters + {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages, + with additional syle information provided by this module. Be careful this is + not compatible with the Emacs mode! *) + +val pp_tag : Pp.tag_handler +(** Returns the name of a style tag that is understandable by the formatters + that have been inititialized through {!init_color_output}. To be used with + {!Pp.pp_with}. *) + +(** {5 Tags} *) + +val error_tag : t +(** Tag used by the {!Pp.msg_error} function. *) + +val warning_tag : t +(** Tag used by the {!Pp.msg_warning} function. *) + +val debug_tag : t +(** Tag used by the {!Pp.msg_debug} function. *) diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml deleted file mode 100644 index fb334c706b..0000000000 --- a/printing/ppstyle.ml +++ /dev/null @@ -1,149 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* assert false - -let set_style tag st = - try tags := String.Map.update tag st !tags with Not_found -> assert false - -let clear_styles () = - tags := String.Map.map (fun _ -> None) !tags - -let dump () = String.Map.bindings !tags - -let parse_config s = - let styles = Terminal.parse s in - let set accu (name, st) = - try String.Map.update name (Some st) accu with Not_found -> accu - in - tags := List.fold_left set !tags styles - -let tag = Pp.Tag.create "ppstyle" - -(** Default tag is to reset everything *) -let default = Terminal.({ - fg_color = Some `DEFAULT; - bg_color = Some `DEFAULT; - bold = Some false; - italic = Some false; - underline = Some false; - negative = Some false; -}) - -let empty = Terminal.make () - -let make_style_stack style_tags = - (** Not thread-safe. We should put a lock somewhere if we print from - different threads. Do we? *) - let style_stack = ref [] in - let peek () = match !style_stack with - | [] -> default (** Anomalous case, but for robustness *) - | st :: _ -> st - in - let push tag = - let style = - try - begin match String.Map.find tag style_tags with - | None -> empty - | Some st -> st - end - with Not_found -> empty - in - (** Use the merging of the latest tag and the one being currently pushed. - This may be useful if for instance the latest tag changes the background and - the current one the foreground, so that the two effects are additioned. *) - let style = Terminal.merge (peek ()) style in - let () = style_stack := style :: !style_stack in - Terminal.eval style - in - let pop _ = match !style_stack with - | [] -> - (** Something went wrong, we fallback *) - Terminal.eval default - | _ :: rem -> - let () = style_stack := rem in - Terminal.eval (peek ()) - in - let clear () = style_stack := [] in - push, pop, clear - -let error_tag = - let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in - make ~style ["message"; "error"] - -let warning_tag = - let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in - make ~style ["message"; "warning"] - -let debug_tag = - let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in - make ~style ["message"; "debug"] - -let pp_tag t = match Pp.Tag.prj t tag with -| None -> "" -| Some key -> key - -let init_color_output () = - let push_tag, pop_tag, clear_tag = make_style_stack !tags in - let tag_handler = { - Format.mark_open_tag = push_tag; - Format.mark_close_tag = pop_tag; - Format.print_open_tag = ignore; - Format.print_close_tag = ignore; - } in - let open Pp_control in - let () = Format.pp_set_mark_tags !std_ft true in - let () = Format.pp_set_mark_tags !err_ft true in - let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in - let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in - let pptag = tag in - let open Pp in - let msg ?header ft strm = - let strm = match header with - | None -> hov 0 strm - | Some (h, t) -> - let tag = Pp.Tag.inj t pptag in - let h = Pp.tag tag (str h ++ str ":") in - hov 0 (h ++ spc () ++ strm) - in - pp_with ~pp_tag ft strm; - Format.pp_print_newline ft (); - Format.pp_print_flush ft (); - (** In case something went wrong, we reset the stack *) - clear_tag (); - in - let logger level strm = match level with - | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm - | Info -> msg !std_ft strm - | Notice -> msg !std_ft strm - | Warning -> - let header = ("Warning", warning_tag) in - Flags.if_warn (fun () -> msg ~header !err_ft strm) () - | Error -> msg ~header:("Error", error_tag) !err_ft strm - in - let () = set_logger logger in - () diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli deleted file mode 100644 index f5d6184cb1..0000000000 --- a/printing/ppstyle.mli +++ /dev/null @@ -1,70 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string list -> t -(** Create a new tag with the given name. Each name must be unique. The optional - style is taken as the default one. *) - -val repr : t -> string list -(** Gives back the original name of the style tag where each string has been - concatenated and separated with a dot. *) - -val tag : t Pp.Tag.key -(** An annotation for styles *) - -(** {5 Manipulating global styles} *) - -val get_style : t -> Terminal.style option -(** Get the style associated to a tag. *) - -val set_style : t -> Terminal.style option -> unit -(** Set a style associated to a tag. *) - -val clear_styles : unit -> unit -(** Clear all styles. *) - -val parse_config : string -> unit -(** Add all styles from the given string as parsed by {!Terminal.parse}. - Unregistered tags are ignored. *) - -val dump : unit -> (t * Terminal.style option) list -(** Recover the list of known tags together with their current style. *) - -(** {5 Setting color output} *) - -val init_color_output : unit -> unit -(** Once called, all tags defined here will use their current style when - printed. To this end, this function redefines the loggers used when sending - messages to the user. The program will in particular use the formatters - {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages, - with additional syle information provided by this module. Be careful this is - not compatible with the Emacs mode! *) - -val pp_tag : Pp.tag_handler -(** Returns the name of a style tag that is understandable by the formatters - that have been inititialized through {!init_color_output}. To be used with - {!Pp.pp_with}. *) - -(** {5 Tags} *) - -val error_tag : t -(** Tag used by the {!Pp.msg_error} function. *) - -val warning_tag : t -(** Tag used by the {!Pp.msg_warning} function. *) - -val debug_tag : t -(** Tag used by the {!Pp.msg_debug} function. *) diff --git a/printing/printing.mllib b/printing/printing.mllib index 7b4c71a8b2..652a34fa1f 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,6 +1,5 @@ Genprint Pputils -Ppstyle Ppannotation Ppconstr Ppconstrsig diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d88ba23ea9..5b330cd252 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -20,12 +20,6 @@ let () = at_exit flush_all let ( / ) = Filename.concat -let fatal_error info anomaly = - let msg = info ++ fnl () in - pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; - flush_all (); - exit (if anomaly then 129 else 1) - let get_version_date () = try let ch = open_in (Envars.coqlib () / "revision") in -- cgit v1.2.3 From 9c7b70032972ed613bcca02cceedcd33c240f7a8 Mon Sep 17 00:00:00 2001 From: Thomas Sibut-Pinote Date: Tue, 23 Jun 2015 14:57:14 +0200 Subject: Wrapped the declare_object function to pretty-print anomalies at loading time. --- library/libobject.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/library/libobject.ml b/library/libobject.ml index 74930d76ec..2ee57baf9c 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -101,7 +101,13 @@ let declare_object_full odecl = dyn_rebuild_function = rebuild }; (infun,outfun) -let declare_object odecl = fst (declare_object_full odecl) +(* The "try .. with .. " allows for correct printing when calling + declare_object a loading time. +*) + +let declare_object odecl = + try fst (declare_object_full odecl) + with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) -- cgit v1.2.3 From 679e49dbdc1448c65122eecd24783eb35376d492 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 21:01:42 +0100 Subject: Adding a more efficient representation of OCaml objects in votour. --- Makefile.build | 2 +- checker/analyze.ml | 350 ++++++++++++++++++++++++++++++++++++++++++++++++++++ checker/analyze.mli | 35 ++++++ checker/votour.ml | 89 +++++++++++-- 4 files changed, 464 insertions(+), 12 deletions(-) create mode 100644 checker/analyze.ml create mode 100644 checker/analyze.mli diff --git a/Makefile.build b/Makefile.build index 92c0d46f24..16c5730865 100644 --- a/Makefile.build +++ b/Makefile.build @@ -654,7 +654,7 @@ $(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) # votour: a small vo explorer (based on the checker) -bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml +bin/votour: lib/cObj$(BESTOBJ) checker/analyze$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I checker,) diff --git a/checker/analyze.ml b/checker/analyze.ml new file mode 100644 index 0000000000..c48b830119 --- /dev/null +++ b/checker/analyze.ml @@ -0,0 +1,350 @@ +(** Headers *) + +let prefix_small_block = 0x80 +let prefix_small_int = 0x40 +let prefix_small_string = 0x20 + +let code_int8 = 0x00 +let code_int16 = 0x01 +let code_int32 = 0x02 +let code_int64 = 0x03 +let code_shared8 = 0x04 +let code_shared16 = 0x05 +let code_shared32 = 0x06 +let code_double_array32_little = 0x07 +let code_block32 = 0x08 +let code_string8 = 0x09 +let code_string32 = 0x0A +let code_double_big = 0x0B +let code_double_little = 0x0C +let code_double_array8_big = 0x0D +let code_double_array8_little = 0x0E +let code_double_array32_big = 0x0F +let code_codepointer = 0x10 +let code_infixpointer = 0x11 +let code_custom = 0x12 +let code_block64 = 0x13 + +type code_descr = +| CODE_INT8 +| CODE_INT16 +| CODE_INT32 +| CODE_INT64 +| CODE_SHARED8 +| CODE_SHARED16 +| CODE_SHARED32 +| CODE_DOUBLE_ARRAY32_LITTLE +| CODE_BLOCK32 +| CODE_STRING8 +| CODE_STRING32 +| CODE_DOUBLE_BIG +| CODE_DOUBLE_LITTLE +| CODE_DOUBLE_ARRAY8_BIG +| CODE_DOUBLE_ARRAY8_LITTLE +| CODE_DOUBLE_ARRAY32_BIG +| CODE_CODEPOINTER +| CODE_INFIXPOINTER +| CODE_CUSTOM +| CODE_BLOCK64 + +let code_max = 0x13 + +let magic_number = "\132\149\166\190" + +(** Memory reification *) + +type repr = +| RInt of int +| RBlock of (int * int) (* tag × len *) +| RString of string +| RPointer of int +| RCode of int + +type data = +| Int of int (* value *) +| Ptr of int (* pointer *) +| Atm of int (* tag *) +| Fun of int (* address *) + +type obj = +| Struct of int * data array (* tag × data *) +| String of string + +module type Input = +sig + type t + val input_byte : t -> int + val input_binary_int : t -> int +end + +module type S = +sig + type input + val parse : input -> (data * obj array) +end + +module Make(M : Input) = +struct + +open M + +type input = M.t + +let current_offset = ref 0 + +let input_byte chan = + let () = incr current_offset in + input_byte chan + +let input_binary_int chan = + let () = current_offset := !current_offset + 4 in + input_binary_int chan + +let input_char chan = Char.chr (input_byte chan) + +let parse_header chan = + let () = current_offset := 0 in + let magic = String.create 4 in + let () = for i = 0 to 3 do magic.[i] <- input_char chan done in + let length = input_binary_int chan in + let objects = input_binary_int chan in + let size32 = input_binary_int chan in + let size64 = input_binary_int chan in + (magic, length, size32, size64, objects) + +let input_int8s chan = + let i = input_byte chan in + if i land 0x80 = 0 + then i + else i lor ((-1) lsl 8) + +let input_int8u = input_byte + +let input_int16s chan = + let i = input_byte chan in + let j = input_byte chan in + let ans = (i lsl 8) lor j in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 16) + +let input_int16u chan = + let i = input_byte chan in + let j = input_byte chan in + (i lsl 8) lor j + +let input_int32s chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 31) + +let input_int32u chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l + +let input_int64s chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + let ans = + (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor + (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p + in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 63) + +let input_int64u chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor + (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p + +let input_header32 chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let tag = l in + let len = (i lsl 14) lor (j lsl 6) lor (k lsr 2) in + (tag, len) + +let input_header64 chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + let tag = p in + let len = + (i lsl 46) lor (j lsl 38) lor (k lsl 30) lor (l lsl 22) lor + (m lsl 14) lor (n lsl 6) lor (o lsr 2) + in + (tag, len) + +let input_string len chan = + let ans = String.create len in + for i = 0 to pred len do + ans.[i] <- input_char chan; + done; + ans + +let parse_object chan = + let data = input_byte chan in + if prefix_small_block <= data then + let tag = data land 0x0F in + let len = (data lsr 4) land 0x07 in + RBlock (tag, len) + else if prefix_small_int <= data then + RInt (data land 0x3F) + else if prefix_small_string <= data then + let len = data land 0x1F in + RString (input_string len chan) + else if data > code_max then + assert false + else match (Obj.magic data) with + | CODE_INT8 -> + RInt (input_int8s chan) + | CODE_INT16 -> + RInt (input_int16s chan) + | CODE_INT32 -> + RInt (input_int32s chan) + | CODE_INT64 -> + RInt (input_int64s chan) + | CODE_SHARED8 -> + RPointer (input_int8u chan) + | CODE_SHARED16 -> + RPointer (input_int16u chan) + | CODE_SHARED32 -> + RPointer (input_int32u chan) + | CODE_BLOCK32 -> + RBlock (input_header32 chan) + | CODE_BLOCK64 -> + RBlock (input_header64 chan) + | CODE_STRING8 -> + let len = input_int8u chan in + RString (input_string len chan) + | CODE_STRING32 -> + let len = input_int32u chan in + RString (input_string len chan) + | CODE_CODEPOINTER -> + let addr = input_int32u chan in + for i = 0 to 15 do ignore (input_byte chan); done; + RCode addr + | CODE_DOUBLE_ARRAY32_LITTLE + | CODE_DOUBLE_BIG + | CODE_DOUBLE_LITTLE + | CODE_DOUBLE_ARRAY8_BIG + | CODE_DOUBLE_ARRAY8_LITTLE + | CODE_DOUBLE_ARRAY32_BIG + | CODE_INFIXPOINTER + | CODE_CUSTOM -> + Printf.eprintf "Unhandled code %04x\n%!" data; assert false + +let parse chan = + let (magic, len, _, _, size) = parse_header chan in + let () = assert (magic = magic_number) in + let memory = Array.make size (Struct ((-1), [||])) in + let current_object = ref 0 in + let fill_obj = function + | RPointer n -> + let data = Ptr (!current_object - n) in + data, None + | RInt n -> + let data = Int n in + data, None + | RString s -> + let data = Ptr !current_object in + let () = memory.(!current_object) <- String s in + let () = incr current_object in + data, None + | RBlock (tag, 0) -> + (* Atoms are never shared *) + let data = Atm tag in + data, None + | RBlock (tag, len) -> + let data = Ptr !current_object in + let nblock = Array.make len (Atm (-1)) in + let () = memory.(!current_object) <- Struct (tag, nblock) in + let () = incr current_object in + data, Some nblock + | RCode addr -> + let data = Fun addr in + data, None + in + + let rec fill block off accu = + if Array.length block = off then + match accu with + | [] -> () + | (block, off) :: accu -> fill block off accu + else + let data, nobj = fill_obj (parse_object chan) in + let () = block.(off) <- data in + let block, off, accu = match nobj with + | None -> block, succ off, accu + | Some nblock -> nblock, 0, ((block, succ off) :: accu) + in + fill block off accu + in + let ans = [|Atm (-1)|] in + let () = fill ans 0 [] in + (ans.(0), memory) + +end + +module IChannel = +struct + type t = in_channel + let input_byte = Pervasives.input_byte + let input_binary_int = Pervasives.input_binary_int +end + +module IString = +struct + type t = (string * int ref) + + let input_byte (s, off) = + let ans = Char.code (s.[!off]) in + let () = incr off in + ans + + let input_binary_int chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 31) + +end + +module PChannel = Make(IChannel) +module PString = Make(IString) + +let parse_channel = PChannel.parse +let parse_string s = PString.parse (s, ref 0) diff --git a/checker/analyze.mli b/checker/analyze.mli new file mode 100644 index 0000000000..42efcf01df --- /dev/null +++ b/checker/analyze.mli @@ -0,0 +1,35 @@ +type data = +| Int of int +| Ptr of int +| Atm of int (* tag *) +| Fun of int (* address *) + +type obj = +| Struct of int * data array (* tag × data *) +| String of string + +val parse_channel : in_channel -> (data * obj array) +val parse_string : string -> (data * obj array) + +(** {6 Functorized version} *) + +module type Input = +sig + type t + val input_byte : t -> int + (** Input a single byte *) + val input_binary_int : t -> int + (** Input a big-endian 31-bits signed integer *) +end +(** Type of inputs *) + +module type S = +sig + type input + val parse : input -> (data * obj array) + (** Return the entry point and the reification of the memory out of a + marshalled structure. *) +end + +module Make (M : Input) : S with type input = M.t +(** Functorized version of the previous code. *) diff --git a/checker/votour.ml b/checker/votour.ml index bb8e067024..4aecb28f20 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -21,32 +21,91 @@ sig type obj val input : in_channel -> obj val repr : obj -> obj repr - val size : int list -> int + val size : obj -> int end -module Repr : S = +module ReprObj : S = struct - type obj = Obj.t + type obj = Obj.t * int list let input chan = let obj = input_value chan in let () = CObj.register_shared_size obj in - obj + (obj, []) - let repr obj = + let repr (obj, pos) = if Obj.is_block obj then let tag = Obj.tag obj in if tag = Obj.string_tag then STRING (Obj.magic obj) else if tag < Obj.no_scan_tag then - let data = Obj.dup obj in - let () = Obj.set_tag data 0 in + let init i = (Obj.field obj i, i :: pos) in + let data = Array.init (Obj.size obj) init in BLOCK (tag, Obj.magic data) else OTHER else INT (Obj.magic obj) - let size p = CObj.shared_size_of_pos p + let size (_, p) = CObj.shared_size_of_pos p end +module ReprMem : S = +struct + open Analyze + + type obj = data + + let memory = ref [||] + let sizes = ref [||] + (** size, in words *) + + let ws = Sys.word_size / 8 + + let rec init_size seen = function + | Int _ | Atm _ | Fun _ -> 0 + | Ptr p -> + if seen.(p) then 0 + else + let () = seen.(p) <- true in + match (!memory).(p) with + | Struct (tag, os) -> + let fold accu o = accu + 1 + init_size seen o in + let size = Array.fold_left fold 1 os in + let () = (!sizes).(p) <- size in + size + | String s -> + let size = 2 + (String.length s / ws) in + let () = (!sizes).(p) <- size in + size + + let size = function + | Int _ | Atm _ | Fun _ -> 0 + | Ptr p -> (!sizes).(p) + + let repr = function + | Int i -> INT i + | Atm t -> BLOCK (t, [||]) + | Fun _ -> OTHER + | Ptr p -> + match (!memory).(p) with + | Struct (tag, os) -> BLOCK (tag, os) + | String s -> STRING s + + let input ch = + let obj, mem = parse_channel ch in + let () = memory := mem in + let () = sizes := Array.make (Array.length mem) (-1) in + let seen = Array.make (Array.length mem) false in + let _ = init_size seen obj in + obj + +end + +module Visit (Repr : S) : +sig + val init : unit -> unit + val visit : Values.value -> Repr.obj -> int list -> unit +end = +struct + (** Name of a value *) let rec get_name ?(extra=false) = function @@ -92,7 +151,7 @@ let rec get_details v o = match v, Repr.repr o with let node_info (v,o,p) = get_name ~extra:true v ^ get_details v o ^ - " (size "^ string_of_int (Repr.size p)^"w)" + " (size "^ string_of_int (Repr.size o)^"w)" (** Children of a block : type, object, position. For lists, we collect all elements of the list at once *) @@ -201,6 +260,8 @@ let rec visit v o pos = | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos | Failure _ | Invalid_argument _ -> visit v o pos +end + (** Loading the vo *) type header = { @@ -256,6 +317,12 @@ let visit_vo f = make_seg "STM tasks" (Opt Values.v_stm_seg); make_seg "opaque proofs" Values.v_opaques; |] in + let repr = + if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S) + (** On 32-bit machines, representation may exceed the max size of arrays *) + in + let module Repr = (val repr : S) in + let module Visit = Visit(Repr) in while true do let ch = open_in_bin f in let magic = input_binary_int ch in @@ -279,8 +346,8 @@ let visit_vo f = let seg = int_of_string l in seek_in ch segments.(seg).pos; let o = Repr.input ch in - let () = init () in - visit segments.(seg).typ o [] + let () = Visit.init () in + Visit.visit segments.(seg).typ o [] done let main = -- cgit v1.2.3 From 5e022fcf97e64a2fdb5ca97d7f877557591fc93c Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Wed, 24 Jun 2015 13:17:20 +0200 Subject: Added _CoqProject to the index of the reference manual. --- doc/refman/RefMan-uti.tex | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 94290bc80f..4960542aac 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -11,7 +11,7 @@ with {\ocaml} code statically linked, with the tool {\tt coqmktop}. For example, one can build a native-code \Coq\ toplevel extended with a tactic -which source is in {\tt tactic.ml} with the command +which source is in {\tt tactic.ml} with the command \begin{verbatim} % coqmktop -opt -o mytop.out tactic.cmx \end{verbatim} @@ -49,7 +49,7 @@ which detects the executables containing the word \texttt{coq}. In this case, the debugger is called with the required additional arguments. In other cases, the debugger is simply called without additional arguments. Such a wrapper can be found in the \texttt{dev/} -subdirectory of the sources. +subdirectory of the sources. \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies} \ttindex{coqdep}} @@ -76,7 +76,8 @@ See the man page of {\tt coqdep} for more details and options. \section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile} \ttindex{Makefile} -\ttindex{coq\_Makefile}} +\ttindex{coq\_Makefile} +\ttindex{\_CoqProject}} \paragraph{\_CoqProject} When a proof development becomes a larger project, split into several @@ -212,10 +213,10 @@ Instructions to use it are contained in this file. {\ProofGeneral} is a generic interface for proof assistants based on Emacs. The main idea is that the \Coq\ commands you are editing are sent to a \Coq\ toplevel running behind Emacs and the -answers of the system automatically inserted into other Emacs buffers. +answers of the system automatically inserted into other Emacs buffers. Thus you don't need to copy-paste the \Coq\ material from your files to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some -files. +files. {\ProofGeneral} is developed and distributed independently of the system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!. @@ -242,7 +243,7 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and \RefManCutCommand{ENDREFMAN=\thepage} %END LATEX -%%% Local Variables: +%%% Local Variables: %%% mode: latex %%% TeX-master: t -%%% End: +%%% End: -- cgit v1.2.3 From 04e2316998678c08711bcaa0a0e762f22e90ba60 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Fri, 26 Jun 2015 00:09:51 +0200 Subject: Some edition in the coq_makefile/_CoqProject section. There are still two items I do not undertand fully (the last one about -extra-phony, and the removal of external libraries at make clean time, that I could not reproduce on a toy example. --- doc/refman/RefMan-uti.tex | 136 ++++++++++++++++++++++++++++------------------ 1 file changed, 83 insertions(+), 53 deletions(-) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 4960542aac..a5e2883f55 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -79,72 +79,102 @@ See the man page of {\tt coqdep} for more details and options. \ttindex{coq\_Makefile} \ttindex{\_CoqProject}} -\paragraph{\_CoqProject} -When a proof development becomes a larger project, split into several -files or containing {\ocaml} plugins, files share common options that -must be specified to all the executables used during the development -of the project. It is therefore convenient to write a file that could -be read all the components (the IDE, the compiler, etc.) that -specify all the files and the common options of the project. - -An attempt to set up a format to write project files has been made -from the command line option of the {\Coq} makefile generator -\texttt{coq\_makefile}. It is described by \texttt{\% coq\_makefile - --help}. The default name for the project file understood by -\texttt{coq\_makefile}, \texttt{coqide} and \texttt{Proof General} is -\texttt{\_CoqProject}. - -A minimal usable project file can probably be obtained by the -invocation +A project is a proof development split into several files, possibly +including the sources of some {\ocaml} plugins, that are located (in +various sub-directories of) a certain directory. The +\texttt{coq\_makefile} command allows to generate generic and complete +\texttt{Makefile} files, that can be used to compile the different +components of the project. A \_CoqProject file +specifies both the list of target files relevant to the project +and the common options that should be passed to each executable at +compilation times, for the IDE, etc. + +\paragraph{\_CoqProject file as an argument to coq\_Makefile.} +In particular, a \_CoqProject file contains the relevant +arguments to be passed to the \texttt{coq\_makefile} makefile +generator using for instance the command: + +\begin{quotation} +\texttt{\% coq\_makefile -f \_CoqProject -o Makefile} +\end{quotation} + +This command generates a file \texttt{Makfile} that can be used to +compile all the sources of the current project. It follows the +syntax described by the output of \texttt{\% coq\_makefile --help}. +Once the \texttt{Makefile} file has been generated a first time, it +can be used by the \texttt{make} command to compile part or all of +the project. Note that once it has been generated once, as soon as +\texttt{\_CoqProject} file is updated, the \texttt{Makefile} file is +automatically regenerated by an invocation of \texttt{make}. + +The following command generates a minimal example of +\texttt{\_CoqProject} file: \begin{quotation} \texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name '*.v' -print \} > \_CoqProject} \end{quotation} +when executed at the root of the directory containing the +project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files +that are present in the current directory and its subdirectories. But no +plugin sources is listed. If a \texttt{Makefile} is generated from +this \texttt{\_CoqProject}, the command \texttt{make install} will +install the compiled project in a subdirectory \texttt{MyFancyLib} of +the \texttt{user-contrib} directory (of the user's {\Coq} libraries +location). This subdirectory is created if it does not already exist. + +\paragraph{\_CoqProject file as a configuration for IDEs.} + +A \texttt{\_CoqProject} file can also be used to configure the options +of the \texttt{coqtop} process executed by a user interface. This +allows to import the libraries of the project under a correct name, +both as a developer of the project, working in the directory +containing its sources, and as a user, using the project after +the installation of its libraries. Currently, both CoqIDE and Proof +General (version $\geq$ 4.3pre) support configuration via +\texttt{\_CoqProject} files. + +\paragraph{Remarks.} -While customizing a project file, mind the following requirements: \begin{itemize} -\item {\Coq} files must end in \texttt{.v}, {\ocaml} modules in - \texttt{.ml4} if they require camlp preprocessing (and in - \texttt{.ml} otherwise), {\ocaml} module signatures, library - description and packing files respectively in \texttt{.mli}, - \texttt{.mllib} and \texttt{.mlpack}. - -Any other argument that is not a valid option will be considered as a -subdirectory. A specified subdirectory must have an inner -\texttt{Makefile}. The phony targets \texttt{all} and \texttt{clean} -will recursively call this target in all the subdirectories. - -\item \texttt{-R} and \texttt{-Q} options are for {\Coq}, \texttt{-I} - for {\ocaml}. The same directory may be ``included'' by both. - - Using \texttt{-R} or \texttt{-Q} gives a correct logical path - and a correct installation location to your coq files. -\item dependency on an external library must not be declared using a - \texttt{-Q \dots} in the \texttt{\_CoqProject} to include it in the - path, as the \textit{make clean} command would erase it! Instead, - install your dependency in a place automatically included by - {\Coq}. You can take advantage of the \texttt{COQPATH} variable - (see \ref{envars}) without installation if necessary. -\item Use \texttt{-extra-phony} with no command to add an extra +\item Every {\Coq} files must use a \texttt{.v} file extension. + The {\ocaml} modules must use a \texttt{.ml4} file extension + if they require camlp preprocessing (and in \texttt{.ml} otherwise). + The {\ocaml} module signatures, library + description and packing files must use respectively \texttt{.mli}, + \texttt{.mllib} and \texttt{.mlpack} file extension. + +\item Any argument that is not a valid option is considered as a + subdirectory. Any subdirectory specified in the list of targets must + itself contain a \texttt{Makefile}. + +\item The phony targets \texttt{all} and \texttt{clean} recursively + call their target in every subdirectory. + +\item \texttt{-R} and \texttt{-Q} options are for {\Coq} files, \texttt{-I} + for {\ocaml} ones. A same directory can be passed to both nature of + options, in the same \texttt{\_CoqProject}. + +\item Using \texttt{-R} or \texttt{-Q} is the appropriate way to + obtain both a correct logical path and a correct installation location to + the libraries of a given project. + +\item Dependencies on external libraries to the project must be + declared with care. If in the \texttt{\_CoqProject} file an external + library \texttt{foo} is passed to a \texttt{-Q} option, like in + \texttt{-Q foo}, the subsequent \textit{make clean} command can + erase \textit{foo}. It is hence safer to customize the + \texttt{COQPATH} variable (see \ref{envars}), to include the + location of the required external libraries. + +\item Using \texttt{-extra-phony} with no command adds extra dependencies on already defined rules. For example the following - skeleton appends something to the \texttt{install} rule: + skeleton appends ``something'' to the \texttt{install} rule: \begin{quotation} \texttt{-extra-phony "install" "install-my-stuff" "" -extra-phony "install-my-stuff" "" "something"} \end{quotation} \end{itemize} -\paragraph{Coq\_makefile} -The writing of a generic and complete \texttt{Makefile} may be tedious -work and that's why {\Coq} provides a tool to automate its creation -from the \texttt{\_CoqProject} file, \texttt{coq\_makefile}. - -Use -\begin{quotation} -\texttt{coq\_makefile -f \_CoqProject -o Makefile} -\end{quotation} -to generate a \texttt{Makefile} the first time. \texttt{Makefile} will be -automatically regenerated when \texttt{\_CoqProject} is updated afterward. \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc} \ttindex{coqdoc}} -- cgit v1.2.3 From e7be889cdc86190ab71709a708e4beb6d3040dd8 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Fri, 26 Jun 2015 00:31:27 +0200 Subject: Typos in my previous edition of the reference manual. --- doc/refman/RefMan-uti.tex | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index a5e2883f55..0729391062 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -74,7 +74,9 @@ instead for the \ocaml\ modules dependencies. See the man page of {\tt coqdep} for more details and options. -\section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile} +\section[Creating a {\tt Makefile} for \Coq\ modules] +{Creating a {\tt Makefile} for \Coq\ modules +\label{Makefile} \ttindex{Makefile} \ttindex{coq\_Makefile} \ttindex{\_CoqProject}} @@ -98,7 +100,7 @@ generator using for instance the command: \texttt{\% coq\_makefile -f \_CoqProject -o Makefile} \end{quotation} -This command generates a file \texttt{Makfile} that can be used to +This command generates a file \texttt{Makefile} that can be used to compile all the sources of the current project. It follows the syntax described by the output of \texttt{\% coq\_makefile --help}. Once the \texttt{Makefile} file has been generated a first time, it @@ -115,12 +117,12 @@ The following command generates a minimal example of \end{quotation} when executed at the root of the directory containing the project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files -that are present in the current directory and its subdirectories. But no +that are present in the current directory and its sub-directories. But no plugin sources is listed. If a \texttt{Makefile} is generated from this \texttt{\_CoqProject}, the command \texttt{make install} will -install the compiled project in a subdirectory \texttt{MyFancyLib} of +install the compiled project in a sub-directory \texttt{MyFancyLib} of the \texttt{user-contrib} directory (of the user's {\Coq} libraries -location). This subdirectory is created if it does not already exist. +location). This sub-directory is created if it does not already exist. \paragraph{\_CoqProject file as a configuration for IDEs.} @@ -129,7 +131,7 @@ of the \texttt{coqtop} process executed by a user interface. This allows to import the libraries of the project under a correct name, both as a developer of the project, working in the directory containing its sources, and as a user, using the project after -the installation of its libraries. Currently, both CoqIDE and Proof +the installation of its libraries. Currently, both \CoqIDE{} and Proof General (version $\geq$ 4.3pre) support configuration via \texttt{\_CoqProject} files. @@ -144,11 +146,11 @@ General (version $\geq$ 4.3pre) support configuration via \texttt{.mllib} and \texttt{.mlpack} file extension. \item Any argument that is not a valid option is considered as a - subdirectory. Any subdirectory specified in the list of targets must + sub-directory. Any sub-directory specified in the list of targets must itself contain a \texttt{Makefile}. \item The phony targets \texttt{all} and \texttt{clean} recursively - call their target in every subdirectory. + call their target in every sub-directory. \item \texttt{-R} and \texttt{-Q} options are for {\Coq} files, \texttt{-I} for {\ocaml} ones. A same directory can be passed to both nature of -- cgit v1.2.3 From aac2d2ac490492f8466e1d45ba0079de376fe25a Mon Sep 17 00:00:00 2001 From: Lionel Rieg Date: Thu, 25 Jun 2015 14:58:25 +0200 Subject: Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" --- CHANGES | 1 + doc/refman/RefMan-syn.tex | 9 ++++++++- interp/notation.ml | 13 +++++++++++++ interp/notation.mli | 1 + intf/vernacexpr.mli | 2 +- parsing/g_vernac.ml4 | 12 +++++++----- printing/ppvernac.ml | 6 +++++- stm/texmacspp.ml | 4 +++- toplevel/metasyntax.ml | 9 ++++++++- toplevel/metasyntax.mli | 1 + toplevel/vernacentries.ml | 4 +++- 11 files changed, 51 insertions(+), 11 deletions(-) diff --git a/CHANGES b/CHANGES index b6793e426f..9172195960 100644 --- a/CHANGES +++ b/CHANGES @@ -4,6 +4,7 @@ Changes from V8.5beta2 to ... Vernacular commands - New command "Redirect" to redirect the output of a command to a file. +- New command "Undelimit Scope" to remove the delimiter of a scope. Tactics diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 37cbd1eac1..aabc8a8995 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -757,7 +757,8 @@ ways to change the interpretation of subterms are available. \subsubsection{Local opening of an interpretation scope \label{scopechange} \index{\%} -\comindex{Delimit Scope}} +\comindex{Delimit Scope} +\comindex{Undelimit Scope}} It is possible to locally extend the interpretation scope stack using the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey} @@ -774,6 +775,12 @@ To bind a delimiting key to a scope, use the command \texttt{Delimit Scope} {\scope} \texttt{with} {\ident} \end{quote} +To remove a delimiting key of a scope, use the command + +\begin{quote} +\texttt{Undelimit Scope} {\scope} +\end{quote} + \subsubsection{Binding arguments of a constant to an interpretation scope \comindex{Arguments}} diff --git a/interp/notation.ml b/interp/notation.ml index 555dfa804b..0b5791d32b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -200,6 +200,19 @@ let declare_delimiters scope key = end with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map +let remove_delimiters scope = + let sc = find_scope scope in + let newsc = { sc with delimiters = None } in + match sc.delimiters with + | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".") + | Some key -> + scope_map := String.Map.add scope newsc !scope_map; + try + let _ = ignore (String.Map.find key !delimiters_map) in + delimiters_map := String.Map.remove key !delimiters_map + with Not_found -> + assert false (* A delimiter for scope [scope] should exist *) + let find_delimiters_scope loc key = try String.Map.find key !delimiters_map with Not_found -> diff --git a/interp/notation.mli b/interp/notation.mli index 854c52b2c7..38bd5fc7b8 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -55,6 +55,7 @@ val find_scope : scope_name -> scope (** Declare delimiters for printing *) val declare_delimiters : scope_name -> delimiters -> unit +val remove_delimiters : scope_name -> unit val find_delimiters_scope : Loc.t -> delimiters -> scope_name (** {6 Declare and uses back and forth an interpretation of primitive token } *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index d7b269a1de..0ca3bb35f6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -284,7 +284,7 @@ type vernac_expr = | VernacSyntaxExtension of obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) - | VernacDelimiters of scope_name * string + | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * reference or_by_notation list | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * constr_expr * scope_name option diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e8a1b512c0..fe9c582408 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -96,12 +96,12 @@ GEXTEND Gram | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) - | v = vernac_poly -> v ] + | v = vernac_poly -> v ] ] ; - vernac_poly: + vernac_poly: [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v) - | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) + | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) | v = vernac_aux -> v ] ] ; @@ -146,7 +146,7 @@ GEXTEND Gram ] ] ; - subgoal_command: + subgoal_command: [ [ c = query_command; "." -> begin function | Some (SelectNth g) -> c (Some g) @@ -1043,7 +1043,9 @@ GEXTEND Gram VernacOpenCloseScope (local,(false,sc)) | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> - VernacDelimiters (sc,key) + VernacDelimiters (sc, Some key) + | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT -> + VernacDelimiters (sc, None) | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 smart_global -> VernacBindScope (sc,refl) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 832c08fe0e..4e889e55f0 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -644,11 +644,15 @@ module Make keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc ) - | VernacDelimiters (sc,key) -> + | VernacDelimiters (sc,Some key) -> return ( keyword "Delimit Scope" ++ spc () ++ str sc ++ spc() ++ keyword "with" ++ spc () ++ str key ) + | VernacDelimiters (sc, None) -> + return ( + keyword "Undelimit Scope" ++ spc () ++ str sc + ) | VernacBindScope (sc,cll) -> return ( keyword "Bind Scope" ++ spc () ++ str sc ++ diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 9edc1f1c70..aaa6c2c07d 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -509,8 +509,10 @@ let rec tmpp v loc = | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name [] | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name [] - | VernacDelimiters (name,tag) -> + | VernacDelimiters (name,Some tag) -> xmlScope loc "delimit" name ~attr:["delimiter",tag] [] + | VernacDelimiters (name,None) -> + xmlScope loc "undelimit" name ~attr:[] [] | VernacBindScope (name,l) -> xmlScope loc "bind" name (List.map (function diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 300bf5b490..7616bfff65 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1383,7 +1383,10 @@ let add_infix local ((loc,inf),modifiers) pr sc = (**********************************************************************) (* Delimiters and classes bound to scopes *) -type scope_command = ScopeDelim of string | ScopeClasses of scope_class list +type scope_command = + | ScopeDelim of string + | ScopeClasses of scope_class list + | ScopeRemove let load_scope_command _ (_,(scope,dlm)) = Notation.declare_scope scope @@ -1393,6 +1396,7 @@ let open_scope_command i (_,(scope,o)) = match o with | ScopeDelim dlm -> Notation.declare_delimiters scope dlm | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl + | ScopeRemove -> Notation.remove_delimiters scope let cache_scope_command o = load_scope_command 1 o; @@ -1418,6 +1422,9 @@ let inScopeCommand : scope_name * scope_command -> obj = let add_delimiters scope key = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) +let remove_delimiters scope = + Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove)) + let add_class_scope scope cl = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 38a3775777..f22839f489 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -39,6 +39,7 @@ val add_notation_extra_printing_rule : string -> string -> string -> unit (** Declaring delimiter keys and default scopes *) val add_delimiters : scope_name -> string -> unit +val remove_delimiters : scope_name -> unit val add_class_scope : scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d9f8f52c8..04d572cd33 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -424,7 +424,9 @@ let vernac_syntax_extension locality local = let local = enforce_module_locality locality local in Metasyntax.add_syntax_extension local -let vernac_delimiters = Metasyntax.add_delimiters +let vernac_delimiters sc = function + | Some lr -> Metasyntax.add_delimiters sc lr + | None -> Metasyntax.remove_delimiters sc let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) -- cgit v1.2.3 From ef6459b00999a29183edc09de9035795ff7912e9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 23 Jun 2015 15:39:47 +0200 Subject: Add target to install dev files. --- Makefile.build | 8 ++++++-- Makefile.common | 4 ++++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/Makefile.build b/Makefile.build index 16c5730865..71fd8fb544 100644 --- a/Makefile.build +++ b/Makefile.build @@ -690,13 +690,13 @@ ifeq ($(LOCAL),true) install: @echo "Nothing to install in a local build!" else -install: install-coq install-coqide install-doc-$(WITHDOC) +install: install-coq install-coqide install-doc-$(WITHDOC) install-dev endif install-doc-all: install-doc install-doc-no: -.PHONY: install install-doc-all install-doc-no +.PHONY: install install-doc-all install-doc-no install-dev #These variables are intended to be set by the caller to make #COQINSTALLPREFIX= @@ -750,6 +750,10 @@ install-tools: $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) +install-dev: $(DEVFILES) $(DEVPRINTERS) + $(foreach devf, $(DEVFILES), sed -i -e /\".\"/\"$(FULLCOQLIB)\"/g $(devf)) + $(INSTALLLIB) $(DEVFILES) $(DEVPRINTERS) $(FULLCOQLIB)/dev + # The list of .cmi to install, including the ones obtained # from .mli without .ml, and the ones obtained from .ml without .mli diff --git a/Makefile.common b/Makefile.common index 07df8bb157..5a81dcfbb2 100644 --- a/Makefile.common +++ b/Makefile.common @@ -253,6 +253,10 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \ mutils.cmo micromega.cmo \ sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) +DEVPRINTERS:=dev/vm_printers.ml dev/top_printers.ml + +DEVFILES:=dev/base_include dev/include + DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo -- cgit v1.2.3 From 3e0aa07cfb1d552e11b37aaf5f0224bfb5b47523 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 23 Jun 2015 17:02:50 +0200 Subject: BUGFIX: Three fixes for the price of 1 in sorts.ml: - Proper [family] implementation - Use the tailor made hash function for Sorts.t in two places. --- kernel/sorts.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/kernel/sorts.ml b/kernel/sorts.ml index ae86d686ae..6e6f41e821 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -62,6 +62,8 @@ let is_small = function let family = function | Prop Null -> InProp | Prop Pos -> InSet + | Type u when is_type0m_univ u -> InProp + | Type u when is_type0_univ u -> InSet | Type _ -> InType let family_equal = (==) @@ -76,7 +78,7 @@ let hash = function in combinesmall 1 h | Type u -> - let h = Hashtbl.hash u in (** FIXME *) + let h = Univ.Universe.hash u in combinesmall 2 h module List = struct @@ -101,7 +103,7 @@ module Hsorts = | (Type u1, Type u2) -> u1 == u2 |_ -> false - let hash = Hashtbl.hash (** FIXME *) + let hash = hash end) let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ -- cgit v1.2.3 From d9ac4c22a3a6543959d413120304e356d625c0f9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 23 Jun 2015 15:40:16 +0200 Subject: Fix bug #4254 with the help of J.H. Jourdan 1) We now _assign_ the smallest possible arities to mutual inductive types and eventually add leq constraints on the user given arities. Remove useless limitation on instantiating algebraic universe variables with their least upper bound if they have upper constraints as well. 2) Do not remove non-recursive variables when computing minimal levels of inductives. 3) Avoid modifying user-given arities if not necessary to compute the minimal level of an inductive. 4) We correctly solve the recursive equations taking into account the user-declared level. --- library/universes.ml | 20 +++++++++------- pretyping/evd.ml | 16 +++++++++---- test-suite/bugs/closed/3446.v | 44 ++++++++++++++++++---------------- test-suite/bugs/closed/3922.v | 2 +- test-suite/bugs/closed/4089.v | 2 +- toplevel/command.ml | 56 +++++++++++++++++++++++++++---------------- 6 files changed, 84 insertions(+), 56 deletions(-) diff --git a/library/universes.ml b/library/universes.ml index 16e6ebb029..a3926bc6f2 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -757,7 +757,7 @@ let minimize_univ_variables ctx us algs left right cstrs = if alg then (* u is algebraic: we instantiate it with it's lower bound, if any, or enforce the constraints if it is bounded from the top. *) - instantiate_with_lbound u lbound true (not (Option.is_empty right)) acc + instantiate_with_lbound u lbound true false acc else (* u is non algebraic *) match Universe.level lbound with | Some l -> (* The lowerbound is directly a level *) @@ -767,7 +767,8 @@ let minimize_univ_variables ctx us algs left right cstrs = if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) - instantiate_with_lbound u lbound false (LSet.mem l algs) acc + let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in + instantiate_with_lbound u lbound false false acc else acc, (true, false, lbound) | None -> try @@ -1017,13 +1018,14 @@ let solve_constraints_system levels level_bounds level_min = for i=0 to nind-1 do for j=0 to nind-1 do if not (Int.equal i j) && Int.Set.mem j clos.(i) then - (v.(i) <- Universe.sup v.(i) level_bounds.(j); - level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) + (v.(i) <- Universe.sup v.(i) level_bounds.(j)); + (* level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) *) done; - for j=0 to nind-1 do - match levels.(j) with - | Some u -> v.(i) <- univ_level_rem u v.(i) level_min.(i) - | None -> () - done + (* for j=0 to nind-1 do *) + (* match levels.(j) with *) + (* | Some u when not (Univ.Level.is_small u) -> *) + (* v.(i) <- univ_level_rem u v.(i) level_min.(i) *) + (* | _ -> () *) + (* done *) done; v diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 60b1da7049..168a10df93 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -351,10 +351,7 @@ let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local let evar_universe_context_subst ctx = ctx.uctx_univ_variables let instantiate_variable l b v = - (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *) - (* if Univ.univ_depends (Univ.Universe.make l) b then *) - (* error ("Occur-check in universe variable instantiation") *) - (* else *) v := Univ.LMap.add l (Some b) !v + v := Univ.LMap.add l (Some b) !v exception UniversesDiffer @@ -420,7 +417,16 @@ let process_universe_constraints univs vars alg cstrs = raise UniversesDiffer in Univ.enforce_eq_level l' r' local - | _, _ (* One of the two is algebraic or global *) -> + | Inr (l, loc, alg), Inl r + | Inl r, Inr (l, loc, alg) -> + let inst = Univ.univ_level_rem l r r in + if alg then (instantiate_variable l inst vars; local) + else + let lu = Univ.Universe.make l in + if Univ.univ_level_mem l r then + Univ.enforce_leq inst lu local + else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) + | _, _ (* One of the two is algebraic or global *) -> if Univ.check_eq univs l r then local else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) in diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v index 4f29b76c6e..dce73e1a50 100644 --- a/test-suite/bugs/closed/3446.v +++ b/test-suite/bugs/closed/3446.v @@ -1,28 +1,32 @@ (* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *) -(* Set Asymmetric Patterns. *) -(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *) -(* Notation "A -> B" := (forall (_ : A), B). *) +Module First. +Set Asymmetric Patterns. +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Notation "A -> B" := (forall (_ : A), B). +Set Universe Polymorphism. + -(* Notation "x → y" := (x -> y) *) -(* (at level 99, y at level 200, right associativity): type_scope. *) -(* Record sigT A (P : A -> Type) := *) -(* { projT1 : A ; projT2 : P projT1 }. *) -(* Arguments projT1 {A P} s. *) -(* Arguments projT2 {A P} s. *) -(* Set Universe Polymorphism. *) -(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *) -(* Reserved Notation "x = y" (at level 70, no associativity). *) -(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *) -(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *) -(* Reserved Notation "{ x : A & P }" (at level 0, x at level 99). *) -(* Notation "{ x : A & P }" := (sigT A (fun x => P)) : type_scope. *) +Notation "x → y" := (x -> y) + (at level 99, y at level 200, right associativity): type_scope. +Record sigT A (P : A -> Type) := + { projT1 : A ; projT2 : P projT1 }. +Arguments projT1 {A P} s. +Arguments projT2 {A P} s. +Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). +Reserved Notation "x = y" (at level 70, no associativity). +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). +Notation " x = y " := (paths x y) : type_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. +Reserved Notation "{ x : A & P }" (at level 0, x at level 99). +Notation "{ x : A & P }" := (sigT A (fun x => P)) : type_scope. -(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v & transport _ p (projT2 u) = projT2 v}), u = v. *) -(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *) +Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v & transport _ p (projT2 u) = projT2 v}), u = v. +Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). -(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *) -(* @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *) +Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := + @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). +End First. Set Asymmetric Patterns. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 9320848910..0ccc92067d 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -43,7 +43,7 @@ Notation IsHProp := (IsTrunc -1). Monomorphic Axiom dummy_funext_type : Type0. Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Record TruncType (n : trunc_index) := BuildTruncType { diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index 1449f242b4..c6cb9c35e6 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -163,7 +163,7 @@ Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope. Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Ltac done := diff --git a/toplevel/command.ml b/toplevel/command.ml index 1b396d57ba..77339aef44 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -402,20 +402,33 @@ let extract_level env evd min tys = sign_level env evd ((Anonymous, None, concl) :: ctx)) tys in sup_list min sorts +let is_flexible_sort evd u = + match Univ.Universe.level u with + | Some l -> Evd.is_flexible_level evd l + | None -> false + let inductive_levels env evdref poly arities inds = - let destarities = List.map (Reduction.dest_arity env) arities in - let levels = List.map (fun (ctx,a) -> + let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in + let levels = List.map (fun (x,(ctx,a)) -> if a = Prop Null then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = CList.split3 - (List.map2 (fun (_,tys,_) (ctx,du) -> + (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> let len = List.length tys in + let minlev = Sorts.univ_of_sort du in let minlev = if len > 1 && not (is_impredicative env du) then - Univ.type0_univ - else Univ.type0m_univ + Univ.sup minlev Univ.type0_univ + else minlev + in + let minlev = + (** Indices contribute. *) + if Indtypes.is_indices_matter () && List.length ctx > 0 then ( + let ilev = sign_level env !evdref ctx in + Univ.sup ilev minlev) + else minlev in let clev = extract_level env !evdref minlev tys in (clev, minlev, len)) inds destarities) @@ -425,32 +438,25 @@ let inductive_levels env evdref poly arities inds = let levels' = Universes.solve_constraints_system (Array.of_list levels) (Array.of_list cstrs_levels) (Array.of_list min_levels) in - let evd = - CList.fold_left3 (fun evd cu (ctx,du) len -> + let evd, arities = + CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative env du then (** Any product is allowed here. *) - evd + evd, arity :: arities else (** If in a predicative sort, or asked to infer the type, we take the max of: - indices (if in indices-matter mode) - constructors - Type(1) if there is more than 1 constructor *) - let evd = - (** Indices contribute. *) - if Indtypes.is_indices_matter () && List.length ctx > 0 then ( - let ilev = sign_level env !evdref ctx in - Evd.set_leq_sort env evd (Type ilev) du) - else evd - in (** Constructors contribute. *) let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) else evd - else - Evd.set_leq_sort env evd (Type cu) du + else evd + (* Evd.set_leq_sort env evd (Type cu) du *) in let evd = if len >= 2 && Univ.is_type0m_univ cu then @@ -459,9 +465,19 @@ let inductive_levels env evdref poly arities inds = land in Prop directly (no informative arguments as well). *) Evd.set_leq_sort env evd (Prop Pos) du else evd - in evd) - !evdref (Array.to_list levels') destarities sizes - in evdref := evd; arities + in + (* let arity = it_mkProd_or_LetIn (mkType cu) ctx in *\) *) + let duu = Sorts.univ_of_sort du in + let evd = + if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then + if is_flexible_sort evd duu then + Evd.set_eq_sort env evd (Prop Null) du + else evd + else Evd.set_eq_sort env evd (Type cu) du + in + (evd, arity :: arities)) + (!evdref,[]) (Array.to_list levels') destarities sizes + in evdref := evd; List.rev arities let check_named (loc, na) = match na with | Name _ -> () -- cgit v1.2.3 From a0b48c4d55cd18655d8e79e6d66b0a0a0651fe3d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 23 Jun 2015 17:08:38 +0200 Subject: Share prop/set values in sorts.ml. --- kernel/sorts.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 6e6f41e821..e2854abfd3 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -26,8 +26,8 @@ let univ_of_sort = function | Prop Null -> Universe.type0m let sort_of_univ u = - if is_type0m_univ u then Prop Null - else if is_type0_univ u then Prop Pos + if is_type0m_univ u then prop + else if is_type0_univ u then set else Type u let compare s1 s2 = -- cgit v1.2.3 From 902ce91fd6006e6df57a8d5133676981967d49b4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 28 Jun 2015 15:02:22 +0200 Subject: Reinstall Set Printing Universes option overwritten by Maxime! --- toplevel/vernacentries.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 04d572cd33..2af28de982 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1433,6 +1433,15 @@ let _ = optread = Pp_control.get_margin; optwrite = Pp_control.set_margin } +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of universes"; + optkey = ["Printing";"Universes"]; + optread = (fun () -> !Constrextern.print_universes); + optwrite = (fun b -> Constrextern.print_universes:=b) } + let _ = declare_bool_option { optsync = true; -- cgit v1.2.3 From 02663c526a3fd347fad803eb664d22e6b5c088ad Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 28 Jun 2015 15:23:00 +0200 Subject: Fix incompleteness of conversion used by evarconv In case we need to backtrack on universe inconsistencies when converting two (incompatible) instances of the same constant and unfold them. Bug reported by Amin Timany. --- pretyping/reductionops.ml | 4 +++- test-suite/success/polymorphism.v | 16 ++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index dd671f111e..dc70f36ccf 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1287,7 +1287,9 @@ let sigma_compare_sorts env pb s0 s1 sigma = let sigma_compare_instances flex i0 i1 sigma = try Evd.set_eq_instances ~flex sigma i0 i1 - with Evd.UniversesDiffer -> raise Reduction.NotConvertible + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 9167c9fcbf..dc22b03f2d 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -292,3 +292,19 @@ Section foo2. Context `{forall A B, Funext A B}. Print Universes. End foo2. + +Module eta. +Set Universe Polymorphism. + +Set Printing Universes. + +Axiom admit : forall A, A. +Record R := {O : Type}. + +Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}. +Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl. +Definition RLRL' : forall x : R, RL x = RL (RL x). + intros. apply eq_refl. +Qed. + +End eta. -- cgit v1.2.3