Skip to content

Commit a7d2fe2

Browse files
W95PspW95Psp
authored
Merge pull request #1556 from cryspen/fix-1453
Nix: un-pin ocamlgraph
2 parents 5736c16 + 03e1a6a commit a7d2fe2

File tree

85 files changed

+898
-866
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

85 files changed

+898
-866
lines changed

‎.github/workflows/install_and_test.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ jobs:
1818
with:
1919
name: hax
2020
skipPush: true
21+
extraPullNames: fstar-nix-versions, z3-nix-versions
22+
2123
- name: Build
2224
run: nix build -L
2325

‎engine/.ocamlformat‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
11
profile = default
2-
version = 0.26.2
2+
version = 0.27.0

‎engine/backends/coq/coq/coq_backend.ml‎

Lines changed: 31 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -18,34 +18,35 @@ include
1818
end)
1919

2020
module SubtypeToInputLanguage
21-
(FA : Features.T
22-
with type mutable_reference = Features.Off.mutable_reference
23-
and type continue = Features.Off.continue
24-
and type break = Features.Off.break
25-
and type mutable_reference = Features.Off.mutable_reference
26-
and type mutable_pointer = Features.Off.mutable_pointer
27-
and type mutable_variable = Features.Off.mutable_variable
28-
and type reference = Features.Off.reference
29-
and type raw_pointer = Features.Off.raw_pointer
30-
and type early_exit = Features.Off.early_exit
31-
and type question_mark = Features.Off.question_mark
32-
and type as_pattern = Features.Off.as_pattern
33-
and type lifetime = Features.Off.lifetime
34-
and type monadic_action = Features.Off.monadic_action
35-
and type arbitrary_lhs = Features.Off.arbitrary_lhs
36-
and type nontrivial_lhs = Features.Off.nontrivial_lhs
37-
and type block = Features.Off.block
38-
and type quote = Features.Off.quote
39-
and type dyn = Features.Off.dyn
40-
and type match_guard = Features.Off.match_guard
41-
and type trait_item_default = Features.Off.trait_item_default
42-
and type unsafe = Features.Off.unsafe
43-
and type loop = Features.Off.loop
44-
and type for_loop = Features.Off.for_loop
45-
and type while_loop = Features.Off.while_loop
46-
and type for_index_loop = Features.Off.for_index_loop
47-
and type state_passing_loop = Features.Off.state_passing_loop
48-
and type fold_like_loop = Features.Off.fold_like_loop) =
21+
(FA :
22+
Features.T
23+
with type mutable_reference = Features.Off.mutable_reference
24+
and type continue = Features.Off.continue
25+
and type break = Features.Off.break
26+
and type mutable_reference = Features.Off.mutable_reference
27+
and type mutable_pointer = Features.Off.mutable_pointer
28+
and type mutable_variable = Features.Off.mutable_variable
29+
and type reference = Features.Off.reference
30+
and type raw_pointer = Features.Off.raw_pointer
31+
and type early_exit = Features.Off.early_exit
32+
and type question_mark = Features.Off.question_mark
33+
and type as_pattern = Features.Off.as_pattern
34+
and type lifetime = Features.Off.lifetime
35+
and type monadic_action = Features.Off.monadic_action
36+
and type arbitrary_lhs = Features.Off.arbitrary_lhs
37+
and type nontrivial_lhs = Features.Off.nontrivial_lhs
38+
and type block = Features.Off.block
39+
and type quote = Features.Off.quote
40+
and type dyn = Features.Off.dyn
41+
and type match_guard = Features.Off.match_guard
42+
and type trait_item_default = Features.Off.trait_item_default
43+
and type unsafe = Features.Off.unsafe
44+
and type loop = Features.Off.loop
45+
and type for_loop = Features.Off.for_loop
46+
and type while_loop = Features.Off.while_loop
47+
and type for_index_loop = Features.Off.for_index_loop
48+
and type state_passing_loop = Features.Off.state_passing_loop
49+
and type fold_like_loop = Features.Off.fold_like_loop) =
4950
struct
5051
module FB = InputLanguage
5152

@@ -67,8 +68,8 @@ end
6768
module CoqNamePolicy = struct
6869
include Concrete_ident.DefaultNamePolicy
6970

70-
(** List of all words that have a special meaning in the target
71-
language, and that should thus be escaped. *)
71+
(** List of all words that have a special meaning in the target language, and
72+
that should thus be escaped. *)
7273
let reserved_words : string Hash_set.t =
7374
Hash_set.of_list
7475
(module String)

‎engine/backends/coq/coq_ast.ml‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -182,7 +182,11 @@ functor
182182
(a_ty_str ^ " " ^ "->" ^ " " ^ b_ty_str, true)
183183
| AST.ArrayTy (t, l) ->
184184
let ty_str = ty_to_string_with_paren t in
185-
("nseq" ^ " " ^ ty_str ^ " " ^ (* Int.to_string *) l, true)
185+
( "nseq" ^ " " ^ ty_str ^ " "
186+
^
187+
(* Int.to_string *)
188+
l,
189+
true )
186190
| AST.SliceTy t ->
187191
let ty_str = ty_to_string_with_paren t in
188192
("seq" ^ " " ^ ty_str, true)
@@ -261,7 +265,7 @@ functor
261265
| Const_char c -> Int.to_string c (* TODO *)
262266
| Const_int (i, { size; _ }) ->
263267
Lib.Notation.int_repr (int_size_to_string size) i
264-
(* *)
268+
(* *)
265269
| Const_bool b -> Bool.to_string b
266270

267271
let rec pat_to_string (x : AST.pat) (is_top_expr : bool) depth : string =

‎engine/backends/coq/ssprove/ssprove_backend.ml‎

Lines changed: 22 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -24,27 +24,28 @@ include
2424
end)
2525

2626
module SubtypeToInputLanguage
27-
(FA : Features.T
28-
with type mutable_reference = Features.Off.mutable_reference
29-
and type continue = Features.Off.continue
30-
and type break = Features.Off.break
31-
and type mutable_pointer = Features.Off.mutable_pointer
32-
and type mutable_variable = Features.Off.mutable_variable
33-
and type reference = Features.Off.reference
34-
and type raw_pointer = Features.Off.raw_pointer
35-
and type early_exit = Features.Off.early_exit
36-
and type question_mark = Features.Off.question_mark
37-
and type as_pattern = Features.Off.as_pattern
38-
and type lifetime = Features.Off.lifetime
39-
and type monadic_action = Features.Off.monadic_action
40-
and type arbitrary_lhs = Features.Off.arbitrary_lhs
41-
and type nontrivial_lhs = Features.Off.nontrivial_lhs
42-
and type quote = Features.Off.quote
43-
and type block = Features.Off.block
44-
and type dyn = Features.Off.dyn
45-
and type match_guard = Features.Off.match_guard
46-
and type trait_item_default = Features.Off.trait_item_default
47-
and type unsafe = Features.Off.unsafe) =
27+
(FA :
28+
Features.T
29+
with type mutable_reference = Features.Off.mutable_reference
30+
and type continue = Features.Off.continue
31+
and type break = Features.Off.break
32+
and type mutable_pointer = Features.Off.mutable_pointer
33+
and type mutable_variable = Features.Off.mutable_variable
34+
and type reference = Features.Off.reference
35+
and type raw_pointer = Features.Off.raw_pointer
36+
and type early_exit = Features.Off.early_exit
37+
and type question_mark = Features.Off.question_mark
38+
and type as_pattern = Features.Off.as_pattern
39+
and type lifetime = Features.Off.lifetime
40+
and type monadic_action = Features.Off.monadic_action
41+
and type arbitrary_lhs = Features.Off.arbitrary_lhs
42+
and type nontrivial_lhs = Features.Off.nontrivial_lhs
43+
and type quote = Features.Off.quote
44+
and type block = Features.Off.block
45+
and type dyn = Features.Off.dyn
46+
and type match_guard = Features.Off.match_guard
47+
and type trait_item_default = Features.Off.trait_item_default
48+
and type unsafe = Features.Off.unsafe) =
4849
struct
4950
module FB = InputLanguage
5051

‎engine/backends/fstar/fstar_backend.ml‎

Lines changed: 32 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -20,31 +20,32 @@ include
2020
end)
2121

2222
module SubtypeToInputLanguage
23-
(FA : Features.T
24-
with type mutable_reference = Features.Off.mutable_reference
25-
and type continue = Features.Off.continue
26-
and type break = Features.Off.break
27-
and type mutable_reference = Features.Off.mutable_reference
28-
and type mutable_pointer = Features.Off.mutable_pointer
29-
and type mutable_variable = Features.Off.mutable_variable
30-
and type reference = Features.Off.reference
31-
and type raw_pointer = Features.Off.raw_pointer
32-
and type early_exit = Features.Off.early_exit
33-
and type question_mark = Features.Off.question_mark
34-
and type as_pattern = Features.Off.as_pattern
35-
and type lifetime = Features.Off.lifetime
36-
and type monadic_action = Features.Off.monadic_action
37-
and type arbitrary_lhs = Features.Off.arbitrary_lhs
38-
and type nontrivial_lhs = Features.Off.nontrivial_lhs
39-
and type loop = Features.Off.loop
40-
and type block = Features.Off.block
41-
and type for_loop = Features.Off.for_loop
42-
and type while_loop = Features.Off.while_loop
43-
and type for_index_loop = Features.Off.for_index_loop
44-
and type state_passing_loop = Features.Off.state_passing_loop
45-
and type fold_like_loop = Features.Off.fold_like_loop
46-
and type match_guard = Features.Off.match_guard
47-
and type trait_item_default = Features.Off.trait_item_default) =
23+
(FA :
24+
Features.T
25+
with type mutable_reference = Features.Off.mutable_reference
26+
and type continue = Features.Off.continue
27+
and type break = Features.Off.break
28+
and type mutable_reference = Features.Off.mutable_reference
29+
and type mutable_pointer = Features.Off.mutable_pointer
30+
and type mutable_variable = Features.Off.mutable_variable
31+
and type reference = Features.Off.reference
32+
and type raw_pointer = Features.Off.raw_pointer
33+
and type early_exit = Features.Off.early_exit
34+
and type question_mark = Features.Off.question_mark
35+
and type as_pattern = Features.Off.as_pattern
36+
and type lifetime = Features.Off.lifetime
37+
and type monadic_action = Features.Off.monadic_action
38+
and type arbitrary_lhs = Features.Off.arbitrary_lhs
39+
and type nontrivial_lhs = Features.Off.nontrivial_lhs
40+
and type loop = Features.Off.loop
41+
and type block = Features.Off.block
42+
and type for_loop = Features.Off.for_loop
43+
and type while_loop = Features.Off.while_loop
44+
and type for_index_loop = Features.Off.for_index_loop
45+
and type state_passing_loop = Features.Off.state_passing_loop
46+
and type fold_like_loop = Features.Off.fold_like_loop
47+
and type match_guard = Features.Off.match_guard
48+
and type trait_item_default = Features.Off.trait_item_default) =
4849
struct
4950
module FB = InputLanguage
5051

@@ -949,14 +950,14 @@ struct
949950
match args with
950951
| [] -> typ
951952
| _ ->
952-
let mk namespace effect = F.term_of_lid (namespace @ [ effect ]) in
953+
let mk namespace eff = F.term_of_lid (namespace @ [ eff ]) in
953954
let prims = mk [ "Prims" ] in
954-
let effect =
955+
let eff =
955956
if Option.is_some prepost_bundle then
956957
if is_lemma then mk [] "Lemma" else prims "Pure"
957958
else prims "Tot"
958959
in
959-
F.mk_e_app effect (if is_lemma then List.drop args 1 else typ :: args)
960+
F.mk_e_app eff (if is_lemma then List.drop args 1 else typ :: args)
960961

961962
(** Prints doc comments out of a list of attributes *)
962963
let pdoc_comments attrs =
@@ -1836,7 +1837,7 @@ let string_of_items ~mod_name ~bundles (bo : BackendOptions.t) m items :
18361837
its
18371838
|> List.map ~f:(map_string ~f:String.strip)
18381839
|> List.filter
1839-
~f:(fst >> (function `Impl s | `Intf s -> String.is_empty s) >> not)
1840+
~f:(fst >> ( function `Impl s | `Intf s -> String.is_empty s ) >> not)
18401841
in
18411842
let string_for filter =
18421843
let l =
@@ -1945,7 +1946,8 @@ module TransformToInputLanguage =
19451946
]
19461947
[@ocamlformat "disable"]
19471948

1948-
(** Rewrites `unsize x` to `x <: τ` when `τ` is in the allowlist described by `unsize_identity_typ` *)
1949+
(** Rewrites `unsize x` to `x <: τ` when `τ` is in the allowlist described by
1950+
`unsize_identity_typ` *)
19491951
let unsize_as_identity =
19501952
(* Tells if a unsize should be treated as identity by type *)
19511953
let rec unsize_identity_typ = function

‎engine/backends/proverif/proverif_backend.ml‎

Lines changed: 32 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -19,25 +19,26 @@ include
1919
end)
2020

2121
module SubtypeToInputLanguage
22-
(FA : Features.T
23-
(* type loop = Features.Off.loop *)
24-
(* and type for_loop = Features.Off.for_loop *)
25-
(* and type for_index_loop = Features.Off.for_index_loop *)
26-
(* and type state_passing_loop = Features.Off.state_passing_loop *)
27-
(* and type continue = Features.Off.continue *)
28-
(* and type break = Features.Off.break *)
29-
(* and type mutable_variable = Features.Off.mutable_variable *)
30-
(* and type mutable_reference = Features.Off.mutable_reference *)
31-
(* and type mutable_pointer = Features.Off.mutable_pointer *)
32-
(* and type reference = Features.Off.reference *)
33-
(* and type slice = Features.Off.slice *)
34-
(* and type raw_pointer = Features.Off.raw_pointer *)
35-
with type early_exit = Features.On.early_exit
36-
and type slice = Features.On.slice
37-
and type question_mark = Features.On.question_mark
38-
and type macro = Features.On.macro
39-
and type quote = Features.On.quote
40-
and type construct_base = Features.On.construct_base
22+
(FA :
23+
Features.T
24+
(* type loop = Features.Off.loop *)
25+
(* and type for_loop = Features.Off.for_loop *)
26+
(* and type for_index_loop = Features.Off.for_index_loop *)
27+
(* and type state_passing_loop = Features.Off.state_passing_loop *)
28+
(* and type continue = Features.Off.continue *)
29+
(* and type break = Features.Off.break *)
30+
(* and type mutable_variable = Features.Off.mutable_variable *)
31+
(* and type mutable_reference = Features.Off.mutable_reference *)
32+
(* and type mutable_pointer = Features.Off.mutable_pointer *)
33+
(* and type reference = Features.Off.reference *)
34+
(* and type slice = Features.Off.slice *)
35+
(* and type raw_pointer = Features.Off.raw_pointer *)
36+
with type early_exit = Features.On.early_exit
37+
and type slice = Features.On.slice
38+
and type question_mark = Features.On.question_mark
39+
and type macro = Features.On.macro
40+
and type quote = Features.On.quote
41+
and type construct_base = Features.On.construct_base
4142
(* and type as_pattern = Features.Off.as_pattern *)
4243
(* and type nontrivial_lhs = Features.Off.nontrivial_lhs *)
4344
(* and type arbitrary_lhs = Features.Off.arbitrary_lhs *)
@@ -179,7 +180,8 @@ module Make (Options : OPTS) : MAKE = struct
179180

180181
method pv_const name typ =
181182
string "const" ^^ space ^^ name ^^ colon ^^ space ^^ typ ^^ dot
182-
(** Print a ProVerif constant declaration of the given typ (provided as a document).*)
183+
(** Print a ProVerif constant declaration of the given typ (provided as
184+
a document).*)
183185

184186
method pv_constructor ?(is_data = false) ?(is_typeconverter = false)
185187
name arg_types typ =
@@ -252,8 +254,8 @@ module Make (Options : OPTS) : MAKE = struct
252254

253255
method typed_wildcard = print#wildcard ^^ string ": bitstring"
254256

255-
method tuple_elem_pat'
256-
: Deprecated_generic_printer_base.par_state -> pat' fn =
257+
method tuple_elem_pat' :
258+
Deprecated_generic_printer_base.par_state -> pat' fn =
257259
fun ctx ->
258260
let wrap_parens =
259261
group
@@ -266,8 +268,8 @@ module Make (Options : OPTS) : MAKE = struct
266268
p ^^ colon ^^ space ^^ print#ty ctx typ
267269
| p -> print#pat' ctx p
268270

269-
method tuple_elem_pat
270-
: Deprecated_generic_printer_base.par_state -> pat fn =
271+
method tuple_elem_pat :
272+
Deprecated_generic_printer_base.par_state -> pat fn =
271273
fun ctx { p; span; _ } ->
272274
print#with_span ~span (fun _ -> print#tuple_elem_pat' ctx p)
273275

@@ -657,12 +659,12 @@ module Make (Options : OPTS) : MAKE = struct
657659
^^ underscore ^^ underscore
658660
^^ print#name_of_concrete_ident id
659661

660-
method! doc_construct_inductive
661-
: is_record:bool ->
662-
is_struct:bool ->
663-
constructor:concrete_ident ->
664-
base:document option ->
665-
(global_ident * document) list fn =
662+
method! doc_construct_inductive :
663+
is_record:bool ->
664+
is_struct:bool ->
665+
constructor:concrete_ident ->
666+
base:document option ->
667+
(global_ident * document) list fn =
666668
fun ~is_record ~is_struct:_ ~constructor ~base:_ args ->
667669
if is_record then
668670
print#concrete_ident constructor

‎engine/default.nix‎

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -66,14 +66,7 @@ let
6666
stdio
6767
re
6868
js_of_ocaml
69-
(ocamlgraph.overrideAttrs (_: {
70-
src = fetchFromGitHub {
71-
owner = "maximebuyse";
72-
repo = "ocamlgraph";
73-
rev = "fix-stable-topological-sort";
74-
sha256 = "sha256-l7v7Kxjaz3xP6T91peAzloyusxpsIOYHXLIiiRHa490=";
75-
};
76-
}))
69+
ocamlgraph
7770
] ++
7871
# F* dependencies
7972
[ batteries menhirLib ppx_deriving ppxlib sedlex stdint ];

0 commit comments

Comments
 (0)