more tests

Author: gares

.github/workflows/ci.yml

@@ -28,6 +28,8 @@ jobs:
           opam_file: 'rocq-elpi.opam'
           custom_image: ${{ matrix.image }}
           after_script: |
+            ls -l
+            chmod -R a+w .
             make all-examples
             make all-tests
           export: 'OPAMWITHTEST OPAMIGNORECONSTRAINTS OPAMVERBOSE'  # space-separated list of variables

apps/cs/tests/setup-project.sh

@@ -71,6 +71,7 @@ Inductive large :=
 
 Inductive prim_int := PI (i : PrimInt63.int).
 Inductive prim_float := PF (f : PrimFloat.float).
+Inductive prim_string := PS (s : lib:elpi.pstring).
 
 Record fo_record := { f1 : peano; f2 : unit; }.
 

apps/derive/tests/test_derive_corelib.v

@@ -31,6 +31,7 @@ Elpi derive.eqOK large.
 *)
 Elpi derive.eqOK prim_int.
 Fail Elpi derive.eqOK prim_float.
+Elpi derive.eqOK prim_string.
 Elpi derive.eqOK fo_record.
 Elpi derive.eqOK pa_record.
 Elpi derive.eqOK pr_record.

apps/derive/tests/test_eqOK.v

@@ -24,6 +24,7 @@ Fail Elpi derive.eqType.ast iota.
 Elpi derive.eqType.ast large.
 Elpi derive.eqType.ast prim_int.
 Fail Elpi derive.eqType.ast prim_float.
+Elpi derive.eqType.ast prim_string.
 Elpi derive.eqType.ast fo_record.
 Elpi derive.eqType.ast pa_record.
 Elpi derive.eqType.ast pr_record.

apps/derive/tests/test_eqType_ast.v

@@ -26,6 +26,7 @@ Elpi derive.eqb large.
 *)
 Elpi derive.eqb prim_int.
 Fail Elpi derive.eqb prim_float.
+Elpi derive.eqb prim_string.
 Elpi derive.eqb fo_record.
 Elpi derive.eqb pa_record.
 Elpi derive.eqb pr_record.

apps/derive/tests/test_eqb.v

@@ -32,6 +32,7 @@ Elpi derive.eqbOK large.
 *)
 Elpi derive.eqbOK prim_int.
 Fail Elpi derive.eqbOK prim_float.
+Elpi derive.eqbOK prim_string.
 Elpi derive.eqbOK fo_record.
 Elpi derive.eqbOK pa_record.
 Elpi derive.eqbOK pr_record.

apps/derive/tests/test_eqbOK.v

@@ -37,6 +37,7 @@ Elpi derive.eqbcorrect large.
 *)
 Elpi derive.eqbcorrect prim_int.
 Fail Elpi derive.eqbcorrect prim_float. (* Can not work, we don't have a syntaxtic test *)
+Elpi derive.eqbcorrect prim_string.
 Elpi derive.eqbcorrect fo_record.
 Elpi derive.eqbcorrect pa_record.
 Elpi derive.eqbcorrect pr_record.   

apps/derive/tests/test_eqbcorrect.v

@@ -24,6 +24,7 @@ Fail Elpi derive.fields iota.
 Elpi derive.fields large.
 Elpi derive.fields prim_int.
 Fail Elpi derive.fields prim_float.
+Elpi derive.fields prim_string.
 Elpi derive.fields fo_record.
 Elpi derive.fields pa_record.
 Elpi derive.fields pr_record.

apps/derive/tests/test_fields.v

@@ -28,6 +28,7 @@ Elpi derive.induction iota.
 Elpi derive.induction large.
 Elpi derive.induction prim_int.
 Elpi derive.induction prim_float.
+Elpi derive.induction prim_string.
 Elpi derive.induction fo_record.
 Elpi derive.induction pa_record.
 Elpi derive.induction pr_record.