fmt

.github/workflows/extract_and_run_coq.yml

@@ -6,7 +6,6 @@ jobs:
     runs-on: ubuntu-latest
     container:
       image: coqorg/coq:8.18.0-ocaml-4.13.1-flambda
-      options: --user root
     steps:
     - uses: actions/checkout@v3
     - name: Build

engine/backends/coq/coq/coq_backend.ml

@@ -137,7 +137,8 @@ let dummy_lib =
    Definition ToString_f_to_string (x : string) := x.\n\
    Instance Sized_any : forall {t_A}, t_Sized t_A := {}.\n\
    Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.\n\
-   Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.\n\
+   Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x \
+   => x}.\n\
    Definition t_Slice (T : Type) := list T.\n\
    Definition unsize {T : Type} : list T -> t_Slice T := id.\n"
 
@@ -437,7 +438,7 @@ struct
       method impl_ident ~goal ~name:_ = goal#p
 
       method impl_item ~ii_span:_ ~ii_generics:_ ~ii_v ~ii_ident ~ii_attrs:_ =
-        (ii_ident)#p ^^ space ^^ string ":=" ^^ space ^^ ii_v#p ^^ semi
+        ii_ident#p ^^ space ^^ string ":=" ^^ space ^^ ii_v#p ^^ semi
 
       method impl_item'_IIFn ~body ~params =
         if List.length params == 0 then body#p
@@ -529,7 +530,13 @@ struct
           (braces
              (nest 2
                 (concat_map_with
-                   ~pre:(break 1 ^^ string (String.drop_prefix (U.Concrete_ident_view.to_definition_name name#v) 2) ^^ !^"_")
+                   ~pre:
+                     (break 1
+                     ^^ string
+                          (String.drop_prefix
+                             (U.Concrete_ident_view.to_definition_name name#v)
+                             2)
+                     ^^ !^"_")
                    (fun x -> x#p)
                    items)
              ^^ break 1))
@@ -541,12 +548,10 @@ struct
 
       method item'_Trait ~super:_ ~name ~generics ~items ~safety:_ =
         let _, params, constraints = generics#v in
-        CoqNotation.class_ name#p (concat_map_with ~pre:space
-             (fun x -> parens x#p)
-             params
-          ^^ concat_map_with ~pre:space
-               (fun x -> x#p)
-               constraints) [] !^"Type"
+        CoqNotation.class_ name#p
+          (concat_map_with ~pre:space (fun x -> parens x#p) params
+          ^^ concat_map_with ~pre:space (fun x -> x#p) constraints)
+          [] !^"Type"
           (braces
              (nest 2 (concat_map_with ~pre:(break 1) (fun x -> x#p) items)
              ^^ break 1))
@@ -991,9 +996,7 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list =
            {
              path = mod_name ^ ".v";
              contents =
-               hardcoded_coq_headers ^ "\n"
-               ^ dummy_lib ^ "\n"
-               ^ contents;
+               hardcoded_coq_headers ^ "\n" ^ dummy_lib ^ "\n" ^ contents;
              sourcemap = None;
            }))
   @ [

engine/lib/concrete_ident/concrete_ident.ml

@@ -244,7 +244,7 @@ module View = struct
     let string_of_def_path_item : Imported.def_path_item -> string option =
       function
       | TypeNs s | ValueNs s | MacroNs s | LifetimeNs s -> Some s
-      | Impl ->  Some "impl"
+      | Impl -> Some "impl"
       | AnonConst -> Some "anon_const"
       | _ -> None
 
@@ -560,8 +560,7 @@ let to_debug_string = T.show
 let map_path_strings ~(f : string -> string) (cid : t) : t =
   { cid with def_id = Imported.map_path_strings ~f cid.def_id }
 
-let parent (cid : t) : t =
-  { cid with def_id = Imported.parent cid.def_id }
+let parent (cid : t) : t = { cid with def_id = Imported.parent cid.def_id }
 
 module DefaultNamePolicy = struct
   let reserved_words = Hash_set.create (module String)
@@ -656,7 +655,8 @@ include DefaultViewAPI
 let remove_impl old =
   let new_parent = (parent (parent old)).def_id in
   {
-    kind = Macro; (* Field; *)
+    kind = Macro;
+    (* Field; *)
     def_id =
       {
         new_parent with

examples/coverage/src/test_enum.rs

@@ -35,12 +35,12 @@ fn test() {
             StructLike { value: i32 },
         }
 
-        use Examples::*; // Creates aliases to all variants.
-        let x = UnitLike; // Path expression of the const item.
-        let x = UnitLike {}; // Struct expression.
-        let y = TupleLike(123); // Call expression.
-        let y = TupleLike { 0: 123 }; // Struct expression using integer field names.
-        let z = StructLike { value: 123 }; // Struct expression.
+        // use Examples::*; // Creates aliases to all variants.
+        let x = Examples::UnitLike; // Path expression of the const item.
+        let x = Examples::UnitLike {}; // Struct expression.
+        let y = Examples::TupleLike(123); // Call expression.
+        let y = Examples::TupleLike { 0: 123 }; // Struct expression using integer field names.
+        let z = Examples::StructLike { value: 123 }; // Struct expression.
     }
     {
         #[repr(u8)]

examples/coverage/src/test_instance.rs

@@ -1,21 +1,21 @@
-enum Option<T> {
+enum SomeEnum<T> {
     None,
     Some(T),
 }
 
-trait Clone {
-    fn clone(&self) -> Self;
+trait SomeTrait {
+    fn some_fun(&self) -> Self;
 }
 
-impl<T> Clone for Option<T>
+impl<T> SomeTrait for SomeEnum<T>
 where
-    T: Clone,
+    T: SomeTrait,
 {
     #[inline]
-    fn clone(&self) -> Self {
+    fn some_fun(&self) -> Self {
         match self {
-            Option::Some(x) => Option::Some(x.clone()),
-            Option::None => Option::None,
+            SomeEnum::Some(x) => SomeEnum::Some(x.some_fun()),
+            SomeEnum::None => SomeEnum::None,
         }
     }
 }