Skip to content

Commit 17ef796

Browse files
committed
Use the gospel file in examples
This only tests the `qcheck-stm` plugin, but it was also the only one modified with this new feature.
1 parent b593bae commit 17ef796

File tree

1 file changed

+24
-3
lines changed

1 file changed

+24
-3
lines changed

examples/dune

Lines changed: 24 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,13 @@
88
(:standard -w -69))
99
(package ortac-examples))
1010

11+
(rule
12+
(alias runtest)
13+
(package ortac-examples)
14+
(targets lwt_dllist_spec.gospel)
15+
(action
16+
(run %{bin:gospel} check %{dep:lwt_dllist_spec.mli})))
17+
1118
(rule
1219
(alias runtest)
1320
(mode promote)
@@ -25,7 +32,7 @@
2532
(run
2633
ortac
2734
qcheck-stm
28-
%{dep:lwt_dllist_spec.mli}
35+
%{dep:lwt_dllist_spec.gospel}
2936
"create ()"
3037
"int t"
3138
--include=lwt_dllist_incl
@@ -67,6 +74,13 @@
6774
(libraries varray)
6875
(package ortac-examples))
6976

77+
(rule
78+
(alias runtest)
79+
(package ortac-examples)
80+
(targets varray_spec.gospel)
81+
(action
82+
(run %{bin:gospel} check %{dep:varray_spec.mli})))
83+
7084
(rule
7185
(mode promote)
7286
(alias runtest)
@@ -84,7 +98,7 @@
8498
(run
8599
ortac
86100
qcheck-stm
87-
%{dep:varray_spec.mli}
101+
%{dep:varray_spec.gospel}
88102
"make 42 'a'"
89103
"char t"
90104
--include=varray_incl
@@ -107,6 +121,13 @@
107121
(rule
108122
(copy varray_spec.mli varray_circular_spec.mli))
109123

124+
(rule
125+
(alias runtest)
126+
(package ortac-examples)
127+
(targets varray_circular_spec.gospel)
128+
(action
129+
(run %{bin:gospel} check %{dep:varray_circular_spec.mli})))
130+
110131
(library
111132
(name varray_circular_spec)
112133
(modules varray_circular_spec)
@@ -130,7 +151,7 @@
130151
(run
131152
ortac
132153
qcheck-stm
133-
%{dep:varray_circular_spec.mli}
154+
%{dep:varray_circular_spec.gospel}
134155
"make 42 'a'"
135156
"char t"
136157
--include=varray_incl

0 commit comments

Comments
 (0)