vendor/coq-serapi/tests/quick/ab.v

+Section AB.
+Lemma a: True. Proof. idtac. fail. auto. Qed.
+
+Lemma b: True. Proof. pose proof a as H. auto. Qed.
+End AB.

vendor/coq-serapi/tests/quick/assoc.v

+Require Import List.
+Import ListNotations.
+
+Set Implicit Arguments.
+
+Ltac break_match_hyp :=
+  match goal with
+    | [ H : context [ match ?X with _ => _ end ] |- _] =>
+      match type of X with
+        | sumbool _ _ => destruct X
+        | _ => destruct X eqn:?
+      end
+  end.
+
+Ltac break_match_goal :=
+  match goal with
+    | [ |- context [ match ?X with _ => _ end ] ] =>
+      match type of X with
+        | sumbool _ _ => destruct X
+        | _ => destruct X eqn:?
+      end
+  end.
+
+Ltac break_match := break_match_goal || break_match_hyp.
+
+Section assoc.
+  Variable K V : Type.
+  Variable K_eq_dec : forall k k' : K, {k = k'} + {k <> k'}.
+
+  Fixpoint assoc (l : list (K * V)) (k : K) : option V :=
+    match l with
+      | [] => None
+      | (k', v) :: l' =>
+        if K_eq_dec k k' then
+          Some v
+        else
+          assoc l' k
+    end.
+
+  Definition assoc_default (l : list (K * V)) (k : K) (default : V) : V :=
+    match (assoc l k) with
+      | Some x => x
+      | None => default
+    end.
+
+  Fixpoint assoc_set (l : list (K * V)) (k : K) (v : V) : list (K * V) :=
+    match l with
+      | [] => [(k, v)]
+      | (k', v') :: l' =>
+        if K_eq_dec k k' then
+          (k, v) :: l'
+        else
+          (k', v') :: (assoc_set l' k v)
+    end.
+
+  Fixpoint assoc_del (l : list (K * V)) (k : K) : list (K * V) :=
+    match l with
+      | [] => []
+      | (k', v') :: l' =>
+        if K_eq_dec k k' then
+          assoc_del l' k
+        else
+          (assoc_del l' k)
+    end.
+
+  Lemma get_set_diff :
+    forall k k' v l,
+      k <> k' ->
+      assoc (assoc_set l k v) k' = assoc l k'.
+  Proof using.
+    induction l; intros; simpl; repeat (break_match; simpl); subst; try congruence; auto.
+  Qed.
+
+  Lemma get_del_same :
+    forall k l,
+      assoc (assoc_del l k) k = None.
+  Proof using.
+    induction l; intros; simpl in *.
+    - auto.
+    - repeat break_match; subst; simpl in *; auto.
+      break_if; try congruence.
+  Qed.
+
+  Lemma get_set_diff_default :
+    forall (k k' : K) (v : V) l d,
+      k <> k' ->
+      assoc_default (assoc_set l k v) k' d = assoc_default l k' d.
+  Proof using.
+    unfold assoc_default.
+    intros.
+    repeat break_match; auto;
+    rewrite get_set_diff in * by auto; congruence.
+  Qed.
+End assoc.

vendor/coq-serapi/tests/quick/dune

+(rule
+ (alias runtest)
+ (deps (:input ab.v))
+ (action (ignore-outputs
+           (bash "%{bin:sercomp} --quick %{input}"))))
+
+(rule
+ (alias runtest)
+ (deps (:input assoc.v))
+ (action (ignore-outputs
+           (bash "%{bin:sercomp} --quick %{input}"))))
+
+(rule
+ (alias runtest)
+ (deps (:input ordered.v))
+ (action (ignore-outputs
+           (bash "%{bin:sercomp} --quick %{input}"))))
+
+(rule
+ (alias runtest)
+ (deps (:input reserved.v))
+ (action (ignore-outputs
+           (bash "%{bin:sercomp} --quick %{input}"))))

vendor/coq-serapi/tests/quick/ordered.v

+Require Import List.
+Require Import NArith.
+
+Module Type OrderedTypeAlt.
+ Parameter t : Type.
+
+ Parameter compare : t -> t -> comparison.
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Parameter compare_sym : forall x y, (y?=x) = CompOpp (x?=y).
+ Parameter compare_trans : forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+ Parameter reflect : forall x y, x ?= y = Eq -> x = y.
+End OrderedTypeAlt.
+
+Module Nat_as_OTA <: OrderedTypeAlt.
+  Definition t := nat.
+  Fixpoint compare x y := 
+    match x,y with 
+      | O,O => Eq
+      | O,_ => Lt
+      | _,O => Gt
+      | S x, S y => compare x y
+    end.
+  Lemma compare_sym: forall x y, compare y x = CompOpp (compare x y). 
+  Proof using. induction x; intros y; destruct y; simpl; auto. Qed.
+  Lemma compare_trans: forall c x y z, compare x y = c -> compare y z = c -> compare x z = c. 
+  Proof using.
+    intros c x. revert c.
+    induction x; intros c y z; destruct y; simpl; intro H; auto; subst; try discriminate H;
+      destruct z; simpl; intro H'; eauto; try discriminate H'.
+  Qed.
+  Lemma reflect: forall x y, compare x y = Eq -> x = y.
+  Proof using. induction x; intros y; destruct y; simpl; intro H; auto; discriminate. Qed.
+End Nat_as_OTA.

vendor/coq-serapi/tests/quick/reserved.v

+Require Import List String Ascii.
+Import ListNotations.
+
+Local Open Scope char.
+
+Module chars.
+  Notation lparen := "("%char.
+  Notation rparen := ")"%char.
+  Notation space  := " "%char.
+  Notation newline  := "010"%char.
+
+  Definition reserved (a : ascii) : Prop  :=
+    In a [lparen; rparen; newline; space].
+
+  Definition reserved_dec (a : ascii) : {reserved a} + {~ reserved a}.
+    unfold reserved.
+    apply in_dec.
+    apply ascii_dec.
+  Defined.
+
+  Lemma lparen_reserved : reserved lparen.
+  Proof using. red. intuition. Qed.
+End chars.

vendor/coq-serapi/tests/sername/dune

+(rule
+ (action
+  (with-stdout-to nat_add.log
+   (run sername --de-bruijn --str-pp %{dep:nat_add.sername}))))
+
+(rule
+ (alias runtest)
+ (action (diff nat_add.out nat_add.log)))

vendor/coq-serapi/tests/sername/nat_add.out

+Nat.add: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance())))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance())))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance()))))) ((v(GProd Anonymous Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GProd Anonymous Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))))(loc()))))(loc()))
+Nat.mul: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance())))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance())))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance()))))) ((v(GProd Anonymous Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GProd Anonymous Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))))(loc()))))(loc()))

vendor/coq-serapi/tests/sername/nat_add.sername

+Nat.add
+Nat.mul
+nat

vendor/coq-serapi/tests/sertop/dune

+; Segfault in envs; thanks to Clément Pit-Claudel
+(rule
+ (action
+  (with-stdout-to full_env.log
+   (with-stdin-from full_env.in (run sertop)))))
+
+(rule
+  (targets full_env.out)
+  (mode promote)
+  (action (run gunzip %{dep:full_env.out.gz})))
+
+; Disabled as it is not reliable on different machines, moreover the
+; test size is huge, we should find a better way to test univ.ml
+
+(rule
+ (alias runtest-fragile)
+ (action (diff full_env.out full_env.log)))
+

vendor/coq-serapi/tests/sertop/full_env.in

+("query0"("Add"()"Require Coq.Vectors.Vector.\nRequire Import Coq.Strings.String Coq.Arith.PeanoNat.\nImport EqNotations Vector.VectorNotations."))
+("query1"("Exec""2"))
+("query2"("Query"(("sid""2"))"EGoals"))
+("query3"("Exec""3"))
+("query4"("Query"(("sid""3"))"EGoals"))
+("query5"("Exec""4"))
+("query6"("Query"(("sid""4"))"EGoals"))
+("query7"("Add"()"Lemma map_snoc_1234 :\n  Vector.map (fun x => 2 * x) (cons 1 [2; 3; 4]) = [2; 4; 6; 8].\nProof.\n  cbv -[Vector.map Nat.mul].\n  Fail destruct (Nat.add_1_r 3). (* .messages *)\nAbort."))
+("query8"("Exec""5"))

webpack.config.js

@@ -128,16 +128,6 @@ export default (env, argv) => [
     rules: [ts, css, imgs, vuesfc],
     unknownContextCritical: false  /* for `randombytes` */
   },
-  optimization: {
-    splitChunks: {
-      cacheGroups: {
-        roninVendor: {
-          /* assume all async-import'ed modules are Ronin; there are too many to list */
-          name: 'ronin-p2p'
-        }
-      }
-    }
-  },
   plugins: shims.plugins
            //[new webpack.ProvidePlugin({process: 'process/browser.js',
            //                            Buffer: ['buffer', 'Buffer']})]