Skip to content

Commit 1ee3d6a

Browse files
rlepigrerlepigre
committed
Use cram tests for [tests].
1 parent f306182 commit 1ee3d6a

File tree

102 files changed

+8056
-428
lines changed

Some content is hidden

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

102 files changed

+8056
-428
lines changed

‎Makefile

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,15 +15,16 @@ build:
1515
.PHONY: build
1616

1717
test-core:
18-
@dune build tests
18+
@dune runtest tests
1919
.PHONY: test-core
2020

2121
test-apps:
2222
@dune build $$(find apps -type d -name tests)
2323
.PHONY: test-apps
2424

2525
test:
26-
@dune build $$(find . -type d -name tests)
26+
@dune runtest
27+
@dune build $$(find apps -type d -name tests)
2728
.PHONY: test
2829

2930
examples:

‎_CoqProject

Lines changed: 57 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
11
-arg -w -arg +elpi.deprecated
22

3+
# Plugins.
4+
5+
-I _build/install/default/lib
6+
7+
# Theories
8+
39
-Q theories elpi
410
-Q _build/default/theories elpi
511
-Q elpi elpi_elpi
612
-Q _build/default/elpi elpi_elpi
7-
-Q tests elpi.tests
8-
-Q _build/default/tests elpi.tests
913
-Q examples elpi.examples
1014
-Q _build/default/examples elpi.examples
1115

@@ -53,3 +57,54 @@
5357
-Q _build/default/apps/tc/tests elpi.apps.tc.tests
5458
-Q apps/tc/theories elpi.apps.tc
5559
-Q _build/default/apps/tc/theories elpi.apps.tc
60+
61+
# Cram tests.
62+
63+
-Q tests/link_order5.t elpi.test
64+
-Q tests/checker.t elpi.test
65+
-Q tests/query_extra_dep.t elpi.test
66+
-Q tests/libobject_C.t elpi.test
67+
-Q tests/link_order3.t elpi.test
68+
-Q tests/ltac3.t elpi.test
69+
-Q tests/synterp.t elpi.test
70+
-Q tests/link_order6.t elpi.test
71+
-Q tests/API2.t elpi.test
72+
-Q tests/glob.t elpi.test
73+
-Q tests/require_bad_order.t elpi.test
74+
-Q tests/API_arguments.t elpi.test
75+
-Q tests/link_order9.t elpi.test
76+
-Q tests/API_typecheck.t elpi.test
77+
-Q tests/link_order7.t elpi.test
78+
-Q tests/libobject_A.t elpi.test
79+
-Q tests/libobject_B.t elpi.test
80+
-Q tests/vernacular1.t elpi.test
81+
-Q tests/API_section.t elpi.test
82+
-Q tests/tactic.t elpi.test
83+
-Q tests/link_perf.t elpi.test
84+
-Q tests/API_elaborate.t elpi.test
85+
-Q tests/link_order_import3.t elpi.test
86+
-Q tests/COQ_ELPI_ATTRIBUTES.t elpi.test
87+
-Q tests/elaborator.t elpi.test
88+
-Q tests/HOAS.t elpi.test
89+
-Q tests/API_notations.t elpi.test
90+
-Q tests/arg_HOAS.t elpi.test
91+
-Q tests/link_order_import2.t elpi.test
92+
-Q tests/link_order2.t elpi.test
93+
-Q tests/link_order8.t elpi.test
94+
-Q tests/cache_async.t elpi.test
95+
-Q tests/API_new_pred.t elpi.test
96+
-Q tests/quotation.t elpi.test
97+
-Q tests/ltac2.t elpi.test
98+
-Q tests/perf_calls.t elpi.test
99+
-Q tests/link_order1.t elpi.test
100+
-Q tests/link_order_import0.t elpi.test
101+
-Q tests/ltac.t elpi.test
102+
-Q tests/link_order4.t elpi.test
103+
-Q tests/API_env.t elpi.test
104+
-Q tests/toposort.t elpi.test
105+
-Q tests/link_order_import1.t elpi.test
106+
-Q tests/API_module.t elpi.test
107+
-Q tests/vernacular2.t elpi.test
108+
-Q tests/API.t elpi.test
109+
-Q tests/ctx_cache.t elpi.test
110+
-Q tests/API_TC_CS.t elpi.test

‎tests/API.t/run.t

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
$ . ../setup-project.sh
2+
$ dune build test.vo
3+
Coq version: 8.19.0 = 8 . 19 . 0
4+
Query assignments:
5+
MA = 8
6+
MI = 19
7+
P = 0
8+
V = 8.19.0
9+
hello world
10+
A
11+
B
12+
Query assignments:
13+
GR = «nat»
14+
Query assignments:
15+
GR = «Nat.add»
16+
MP = «Coq.Init.Datatypes»
17+
Query assignments:
18+
A = «test.test.succ»
19+
GR = «Nat.add»
20+
MP = «Coq.Init.Datatypes»
21+
X1 = [loc-gref (const «Nat.add»)]
22+
X2 = [loc-gref (const «Nat.add»)]
23+
X3 = [loc-abbreviation «test.test.succ»]
24+
X4 = [loc-modpath «Coq.Init.Datatypes»]
25+
Universe constraints:
26+
Query assignments:
27+
X = «test.test.1»
28+
Universe constraints:
29+
UNIVERSES:
30+
{test.test.1} |=
31+
ALGEBRAIC UNIVERSES:
32+
{}
33+
FLEXIBLE UNIVERSES:
34+
35+
SORTS:
36+
37+
WEAK CONSTRAINTS:
38+
39+
40+
Query assignments:
41+
X = typ «test.test.2»
42+
Y = typ «test.test.3»
43+
Universe constraints:
44+
UNIVERSES:
45+
{test.test.3 test.test.2} |= test.test.2 <= test.test.3
46+
ALGEBRAIC UNIVERSES:
47+
{}
48+
FLEXIBLE UNIVERSES:
49+
50+
SORTS:
51+
52+
WEAK CONSTRAINTS:
53+
54+
55+
Query assignments:
56+
X = typ «test.test.4»
57+
Y = typ «test.test.5»
58+
Universe constraints:
59+
UNIVERSES:
60+
{test.test.5 test.test.4} |= test.test.4 <= test.test.5
61+
ALGEBRAIC UNIVERSES:
62+
{}
63+
FLEXIBLE UNIVERSES:
64+
65+
SORTS:
66+
67+
WEAK CONSTRAINTS:
68+
69+
70+
Query assignments:
71+
X = typ «test.test.6»
72+
Y = typ «test.test.7»
73+
Z = typ «test.test.8»
74+
Universe constraints:
75+
UNIVERSES:
76+
{test.test.8 test.test.7 test.test.6} |=
77+
test.test.6 <= test.test.8
78+
test.test.7 <= test.test.8
79+
ALGEBRAIC UNIVERSES:
80+
{}
81+
FLEXIBLE UNIVERSES:
82+
83+
SORTS:
84+
85+
WEAK CONSTRAINTS:
86+
87+
88+
Query assignments:
89+
X = typ «test.test.9»
90+
Y = typ «test.test.10»
91+
Universe constraints:
92+
UNIVERSES:
93+
{test.test.10 test.test.9} |= test.test.9 < test.test.10
94+
ALGEBRAIC UNIVERSES:
95+
{}
96+
FLEXIBLE UNIVERSES:
97+
98+
SORTS:
99+
100+
WEAK CONSTRAINTS:
101+
102+
103+
[foo (const «X»), foo (indt «nat»), foo (indt «bool»)]
104+
[foo (indt «nat»), foo (indt «bool»)]
105+
[]
106+
[foo (indt «nat»)]
107+
hello [int 1, int 2, trm (global (indt «nat»)), str x]
108+
coq.pp.box (coq.pp.hv 2)
109+
[coq.pp.str Module, coq.pp.spc, coq.pp.str Foo, coq.pp.spc, coq.pp.str :=,
110+
coq.pp.brk 1 0, coq.pp.str body, coq.pp.spc, coq.pp.str End Foo.]
111+
Module
112+
Foo
113+
:=
114+
body
115+
End Foo.
116+
fix foo (x : ?e3) (y : ?e4) {struct x} : ?e2 :=
117+
match x as x0 return ?e6@{x:=x0} with
118+
| true => S (S (S O))
119+
| false => y
120+
end
121+
fix foo x y {struct x} := if x as x0 return ?e6@{x:=x0} then 3 else y

‎tests/test_API.v renamed to ‎tests/API.t/test.v

File renamed without changes.

‎tests/API2.t/run.t

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
$ . ../setup-project.sh
2+
$ dune build test.vo
3+
Warning: in file test.v, library test_API is required
4+
from root elpi and has not been found in the loadpath!
5+
[module-not-found,filesystem,default]
6+
File "./test.v", line 3, characters 0-27:
7+
Error: Cannot find a physical path bound to logical path
8+
test_API with prefix elpi.
9+
10+
[1]

‎tests/test_API2.v renamed to ‎tests/API2.t/test.v

File renamed without changes.

0 commit comments

Comments
 (0)