From f070949a7559675af3e551e16e5cae95af5d4285 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 11:51:12 +0200 Subject: Do not use the list notation `[]` The rest of the code base uses `nil`, so let's be consistent. Also, this avoids depending on `Import ListNotations`. --- lib/Floats.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'lib') diff --git a/lib/Floats.v b/lib/Floats.v index 13350dd0..00d00a57 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -223,10 +223,10 @@ Definition cons_pl (x: float) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x [])). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x nil)). Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y []))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y nil))). (** For fused multiply-add, the order in which arguments are examined to select a NaN payload varies across platforms. E.g. in [fma x y z], @@ -236,7 +236,7 @@ Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := Definition fma_nan_1 (x y z: float) : {x : float | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c [])))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c nil)))). (** One last wrinkle for fused multiply-add: [fma zero infinity nan] can return either the quiesced [nan], or the default NaN arising out @@ -248,7 +248,7 @@ Definition fma_nan (x y z: float) : {x : float | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z [])) + then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z nil)) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z @@ -1011,20 +1011,20 @@ Definition cons_pl (x: float32) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x [])). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x nil)). Definition binop_nan (x y: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y []))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y nil))). Definition fma_nan_1 (x y z: float32) : {x : float32 | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c [])))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c nil)))). Definition fma_nan (x y z: float32) : {x : float32 | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z [])) + then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z nil)) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z -- cgit From 65ad896aed67aa06845e0b2ac9f7f98179f6e170 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 12:03:05 +0200 Subject: Revert "Do not use the list notation `[]`" On some versions of Coq, "nil" is of type "Rlist"... This reverts commit f070949a7559675af3e551e16e5cae95af5d4285. --- lib/Floats.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'lib') diff --git a/lib/Floats.v b/lib/Floats.v index 00d00a57..13350dd0 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -223,10 +223,10 @@ Definition cons_pl (x: float) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x nil)). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x [])). Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y nil))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y []))). (** For fused multiply-add, the order in which arguments are examined to select a NaN payload varies across platforms. E.g. in [fma x y z], @@ -236,7 +236,7 @@ Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := Definition fma_nan_1 (x y z: float) : {x : float | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c nil)))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c [])))). (** One last wrinkle for fused multiply-add: [fma zero infinity nan] can return either the quiesced [nan], or the default NaN arising out @@ -248,7 +248,7 @@ Definition fma_nan (x y z: float) : {x : float | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z nil)) + then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z [])) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z @@ -1011,20 +1011,20 @@ Definition cons_pl (x: float32) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x nil)). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x [])). Definition binop_nan (x y: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y nil))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y []))). Definition fma_nan_1 (x y z: float32) : {x : float32 | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c nil)))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c [])))). Definition fma_nan (x y z: float32) : {x : float32 | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z nil)) + then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z [])) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z -- cgit From e464549037dcf94494c5aea462e6c3854b44976d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 12:04:38 +0200 Subject: Import ListNotations explicitly So as not to depend on an implicit import from module Program. (See PR #352.) --- lib/Floats.v | 1 + 1 file changed, 1 insertion(+) (limited to 'lib') diff --git a/lib/Floats.v b/lib/Floats.v index 13350dd0..6a126c3f 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -22,6 +22,7 @@ Require Import Binary Bits Core. Require Import IEEE754_extra. Require Import Program. Require Archi. +Import ListNotations. Close Scope R_scope. Open Scope Z_scope. -- cgit From 4a676623badb718da4055b7f26ee05f5097f4e7b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 11:11:27 +0200 Subject: Move Commandline to the lib/ directory The Commandline module is reusable in other projects, and its license (GPL) allows such reuse, so its natural place is in lib/ rather than in driver/ --- lib/Commandline.ml | 141 ++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/Commandline.mli | 55 ++++++++++++++++++++ 2 files changed, 196 insertions(+) create mode 100644 lib/Commandline.ml create mode 100644 lib/Commandline.mli (limited to 'lib') diff --git a/lib/Commandline.ml b/lib/Commandline.ml new file mode 100644 index 00000000..672ed834 --- /dev/null +++ b/lib/Commandline.ml @@ -0,0 +1,141 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Parsing of command-line flags and arguments *) + +open Printf + +type pattern = + | Exact of string + | Prefix of string + | Suffix of string + | Regexp of Str.regexp + +let _Regexp re = Regexp (Str.regexp re) + +type action = + | Set of bool ref + | Unset of bool ref + | Self of (string -> unit) + | String of (string -> unit) + | Integer of (int -> unit) + | Ignore + | Unit of (unit -> unit) + +exception CmdError of string + +let match_pattern text = function + | Exact s -> + text = s + | Prefix pref -> + let lpref = String.length pref and ltext = String.length text in + lpref < ltext && String.sub text 0 lpref = pref + (* strict prefix: no match if pref = text. See below. *) + | Suffix suff -> + let lsuff = String.length suff and ltext = String.length text in + lsuff < ltext && String.sub text (ltext - lsuff) lsuff = suff + (* strict suffix: no match if suff = text, so that e.g. ".c" + causes an error rather than being treated as a C source file. *) + | Regexp re -> + Str.string_match re text 0 + +let rec find_action text = function + | [] -> None + | (pat, act) :: rem -> + if match_pattern text pat then Some act else find_action text rem + +let parse_array spec argv first last = + (* Split the spec into Exact patterns (in a hashtable) and other patterns *) + let exact_cases = (Hashtbl.create 29 : (string, action) Hashtbl.t) in + let rec split_spec = function + | [] -> [] + | (Exact s, act) :: rem -> Hashtbl.add exact_cases s act; split_spec rem + | (pat, act) :: rem -> (pat, act) :: split_spec rem in + let inexact_cases = split_spec spec in + (* Parse the vector of arguments *) + let rec parse i = + if i <= last then begin + let s = argv.(i) in + let optact = + try Some (Hashtbl.find exact_cases s) + with Not_found -> find_action s inexact_cases in + match optact with + | None -> + let msg = sprintf "unknown argument `%s'" s in + raise (CmdError msg) + | Some(Set r) -> + r := true; parse (i+1) + | Some(Unset r) -> + r := false; parse (i+1) + | Some(Self fn) -> + fn s; parse (i+1) + | Some(String fn) -> + if i + 1 <= last then begin + fn argv.(i+1); parse (i+2) + end else begin + let msg = sprintf "option `%s' expects an argument" s in + raise (CmdError msg) + end + | Some(Integer fn) -> + if i + 1 <= last then begin + let n = + try + int_of_string argv.(i+1) + with Failure _ -> + let msg = sprintf "argument to option `%s' must be an integer" s in + raise (CmdError msg) + in + fn n; parse (i+2) + end else begin + let msg = sprintf "option `%s' expects an argument" s in + raise (CmdError msg) + end + | Some (Ignore) -> + if i + 1 <= last then begin + parse (i+2) + end else begin + let msg = sprintf "option `%s' expects an argument" s in + raise (CmdError msg) + end + | Some (Unit f) -> f (); parse (i+1) + end + in parse first + +let argv = + try + Responsefile.expandargv Sys.argv + with Responsefile.Error msg | Sys_error msg -> + eprintf "Error while processing the command line: %s\n" msg; + exit 2 + +let parse_cmdline spec = + parse_array spec argv 1 (Array.length argv - 1) + +let long_int_action key s = + let ls = String.length s + and lkey = String.length key in + assert (ls > lkey); + let s = String.sub s (lkey + 1) (ls - lkey - 1) in + try + int_of_string s + with Failure _ -> + let msg = sprintf "argument to option `%s' must be an integer" key in + raise (CmdError msg) + +let longopt_int key f = + let act s = + let n = long_int_action key s in + f n in + Prefix (key ^ "="),Self act diff --git a/lib/Commandline.mli b/lib/Commandline.mli new file mode 100644 index 00000000..8bb6f18f --- /dev/null +++ b/lib/Commandline.mli @@ -0,0 +1,55 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Parsing of command-line flags and arguments *) + +(* A command-line specification is a list of pairs (pattern, action). + Command-line words are matched against the patterns, and the + corresponding actions are invoked. *) + +type pattern = + | Exact of string (** exactly this string *) + | Prefix of string (** any string starting with this prefix *) + | Suffix of string (** any string ending with this suffix *) + | Regexp of Str.regexp (** any string matching this anchored regexp *) + +val _Regexp: string -> pattern (** text of an [Str] regexp *) + +type action = + | Set of bool ref (** set the given ref to true *) + | Unset of bool ref (** set the given ref to false *) + | Self of (string -> unit) (** call the function with the matched string *) + | String of (string -> unit) (** read next arg as a string, call function *) + | Integer of (int -> unit) (** read next arg as an int, call function *) + | Ignore (** ignore the next arg *) + | Unit of (unit -> unit) (** call the function with unit as argument *) +(* Note on precedence: [Exact] patterns are tried first, then the other + patterns are tried in the order in which they appear in the list. *) + +exception CmdError of string +(** Raise by [parse_cmdline] when an error occurred *) + +val parse_cmdline: (pattern * action) list -> unit +(** [parse_cmdline actions] parses the command line (after @-file expansion) + and performs all [actions]. Raises [CmdError] if an error occurred. +*) + +val longopt_int: string -> (int -> unit) -> pattern * action +(** [longopt_int key fn] generates a pattern and an action for + options of the form [key=] and calls [fn] with the integer argument +*) + +val argv: string array +(** [argv] contains the complete command line after @-file expandsion *) -- cgit From 0eba6f63b6bc458d856e477f6f8ec6b78ef78c58 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 19 May 2020 10:25:45 +0200 Subject: Add a canonical encoding of identifiers as numbers and use it in clightgen (#353) Within CompCert, identifiers (names of C functions, variables, types, etc) are represented by unique positive numbers, sometimes called "atoms". In the original implementation, atoms 1, 2, ..., N are assigned to identifiers as they are encountered. The resulting number are small and are efficient when used as keys in data structures such as PTrees. However, the mapping from C source-level identifiers to atoms differs between compilation units. This is not a problem for CompCert but complicates CompCert-based verification tools that need to combine several compilation units. This commit introduces an alternate implementation of atoms, suggested by Andrew Appel. The choice between implementations is governed by the Boolean reference `Camlcoq.use_canonical_atoms`. In the alternate implementation, identifiers are converted to bit sequences via a Huffman encoding, then the bits are represented as positive numbers. The same identifier is always represented by the same number. However, the numbers are usually bigger than in the original implementation, making PTree operations slower: lookups and updates take time linear in the length of the identifier, instead of logarithmic time in the number of identifiers encountered. The CompCert compiler (the `ccomp` executable) still uses the original implementation, but the `clightgen` tool used in conjunction with the VST program logic can use either implementations: - The alternate "canonical atoms" implementation is used by default, and also if the `-canonical-idents` option is given. - The original implementation is used if the `-short-idents` option is given. Closes: #222 Closes: #311 --- lib/Camlcoq.ml | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 76 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 66322efb..af65b28e 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -282,23 +282,96 @@ type atom = positive let atom_of_string = (Hashtbl.create 17 : (string, atom) Hashtbl.t) let string_of_atom = (Hashtbl.create 17 : (atom, string) Hashtbl.t) let next_atom = ref Coq_xH +let use_canonical_atoms = ref false + +(* If [use_canonical_atoms] is false, strings are numbered from 1 up + in the order in which they are encountered. This produces small + numbers, and is therefore efficient, but the number for a given + string may differ between the compilation of different units. + + If [use_canonical_atoms] is true, strings are Huffman-encoded as bit + sequences, which are then encoded as positive numbers. The same + string is always represented by the same number in all compilation + units. However, the numbers are bigger than in the first + implementation. Also, this places a hard limit on the number of + fresh identifiers that can be generated starting with + [first_unused_ident]. *) + +let rec append_bits_pos nbits n p = + if nbits <= 0 then p else + if n land 1 = 0 + then Coq_xO (append_bits_pos (nbits - 1) (n lsr 1) p) + else Coq_xI (append_bits_pos (nbits - 1) (n lsr 1) p) + +(* The encoding of strings as bit sequences is optimized for C identifiers: + - numbers are encoded as a 6-bit integer between 0 and 9 + - lowercase letters are encoded as a 6-bit integer between 10 and 35 + - uppercase letters are encoded as a 6-bit integer between 36 and 61 + - the underscore character is encoded as the 6-bit integer 62 + - all other characters are encoded as 6 "one" bits followed by + the 8-bit encoding of the character. *) + +let append_char_pos c p = + match c with + | '0'..'9' -> append_bits_pos 6 (Char.code c - Char.code '0') p + | 'a'..'z' -> append_bits_pos 6 (Char.code c - Char.code 'a' + 10) p + | 'A'..'Z' -> append_bits_pos 6 (Char.code c - Char.code 'A' + 36) p + | '_' -> append_bits_pos 6 62 p + | _ -> append_bits_pos 6 63 (append_bits_pos 8 (Char.code c) p) + +(* The empty string is represented as the positive "1", that is, [xH]. *) + +let pos_of_string s = + let rec encode i accu = + if i < 0 then accu else encode (i - 1) (append_char_pos s.[i] accu) + in encode (String.length s - 1) Coq_xH + +let fresh_atom () = + let a = !next_atom in + next_atom := Pos.succ !next_atom; + a let intern_string s = try Hashtbl.find atom_of_string s with Not_found -> - let a = !next_atom in - next_atom := Pos.succ !next_atom; + let a = + if !use_canonical_atoms then pos_of_string s else fresh_atom () in Hashtbl.add atom_of_string s a; Hashtbl.add string_of_atom a s; a + let extern_atom a = try Hashtbl.find string_of_atom a with Not_found -> Printf.sprintf "$%d" (P.to_int a) -let first_unused_ident () = !next_atom +(* Ignoring the terminating "1" bit, canonical encodings of strings can + be viewed as lists of bits, formed by concatenation of 6-bit fragments + (for letters, numbers, and underscore) and 14-bit fragments (for other + characters). Hence, not all positive numbers are canonical encodings: + only those whose log2 is of the form [6n + 14m]. + + Here are the first intervals of positive numbers corresponding to strings: + - [1, 1] for the empty string + - [2^6, 2^7-1] for one "compact" character + - [2^12, 2^13-1] for two "compact" characters + - [2^14, 2^14-1] for one "escaped" character + + Hence, between 2^7 and 2^12 - 1, we have 3968 consecutive positive + numbers that cannot be the encoding of a string. These are the positive + numbers we'll use as temporaries in the SimplExpr pass if canonical + atoms are in use. + + If short atoms are used, we just number the temporaries consecutively + starting one above the last generated atom. +*) + +let first_unused_ident () = + if !use_canonical_atoms + then P.of_int 128 + else !next_atom (* Strings *) -- cgit From 19aed83caebcae1103e0c4f6e200744492f17545 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 24 Apr 2020 15:17:37 +0200 Subject: Use Hashtbl.find_opt. Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt. --- lib/Readconfig.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll index 7b98255e..8abcc407 100644 --- a/lib/Readconfig.mll +++ b/lib/Readconfig.mll @@ -20,7 +20,7 @@ let key_val_tbl : (string, string list) Hashtbl.t = Hashtbl.create 17 let key_val key = - try Some(Hashtbl.find key_val_tbl key) with Not_found -> None + Hashtbl.find_opt key_val_tbl key (* Auxiliaries for parsing *) -- cgit From d9e1175be2e713232d06c80e9aed33032858e9c7 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 18 Sep 2020 16:52:21 +0200 Subject: Simplify two scripts in Zbits (#369) Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity. --- lib/Zbits.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/Zbits.v b/lib/Zbits.v index 27586aff..6f3acaab 100644 --- a/lib/Zbits.v +++ b/lib/Zbits.v @@ -266,7 +266,7 @@ Qed. Remark Ztestbit_shiftin_base: forall b x, Z.testbit (Zshiftin b x) 0 = b. Proof. - intros. rewrite Ztestbit_shiftin. apply zeq_true. omega. + intros. rewrite Ztestbit_shiftin; reflexivity. Qed. Remark Ztestbit_shiftin_succ: @@ -316,7 +316,7 @@ Qed. Remark Ztestbit_base: forall x, Z.testbit x 0 = Z.odd x. Proof. - intros. rewrite Ztestbit_eq. apply zeq_true. omega. + intros. rewrite Ztestbit_eq; reflexivity. Qed. Remark Ztestbit_succ: -- cgit From ab0d9476db875a82cf293623d18552b62f239d5c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 21 Sep 2020 14:15:57 +0200 Subject: Support the use of already-installed MenhirLib and Flocq libraries configure flags -use-external-Flocq and -use external-MenhirLib. --- lib/Floats.v | 3 +-- lib/IEEE754_extra.v | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) (limited to 'lib') diff --git a/lib/Floats.v b/lib/Floats.v index 6a126c3f..b7769420 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -17,8 +17,7 @@ (** Formalization of floating-point numbers, using the Flocq library. *) Require Import Coqlib Zbits Integers. -(*From Flocq*) -Require Import Binary Bits Core. +From Flocq Require Import Binary Bits Core. Require Import IEEE754_extra. Require Import Program. Require Archi. diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index c23149be..18313ec1 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -17,11 +17,11 @@ (** Additional operations and proofs about IEEE-754 binary floating-point numbers, on top of the Flocq library. *) +From Flocq Require Import Core Digits Operations Round Bracket Sterbenz + Binary Round_odd. Require Import Psatz. Require Import Bool. Require Import Eqdep_dec. -(*From Flocq *) -Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd. Local Open Scope Z_scope. -- cgit