Skip to content

Commit

Permalink
Use the gospel file in examples
Browse files Browse the repository at this point in the history
This only tests the `qcheck-stm` plugin, but it was also the only one
modified with this new feature.
  • Loading branch information
n-osborne committed Jan 24, 2024
1 parent b593bae commit d0a9a54
Show file tree
Hide file tree
Showing 4 changed files with 24 additions and 2,939 deletions.
27 changes: 24 additions & 3 deletions examples/dune
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,13 @@
(:standard -w -69))
(package ortac-examples))

(rule
(alias runtest)
(package ortac-examples)
(targets lwt_dllist_spec.gospel)
(action
(run %{bin:gospel} check %{dep:lwt_dllist_spec.mli})))

(rule
(alias runtest)
(mode promote)
Expand All @@ -25,7 +32,7 @@
(run
ortac
qcheck-stm
%{dep:lwt_dllist_spec.mli}
%{dep:lwt_dllist_spec.gospel}
"create ()"
"int t"
--include=lwt_dllist_incl
Expand Down Expand Up @@ -67,6 +74,13 @@
(libraries varray)
(package ortac-examples))

(rule
(alias runtest)
(package ortac-examples)
(targets varray_spec.gospel)
(action
(run %{bin:gospel} check %{dep:varray_spec.mli})))

(rule
(mode promote)
(alias runtest)
Expand All @@ -84,7 +98,7 @@
(run
ortac
qcheck-stm
%{dep:varray_spec.mli}
%{dep:varray_spec.gospel}
"make 42 'a'"
"char t"
--include=varray_incl
Expand All @@ -107,6 +121,13 @@
(rule
(copy varray_spec.mli varray_circular_spec.mli))

(rule
(alias runtest)
(package ortac-examples)
(targets varray_circular_spec.gospel)
(action
(run %{bin:gospel} check %{dep:varray_circular_spec.mli})))

(library
(name varray_circular_spec)
(modules varray_circular_spec)
Expand All @@ -130,7 +151,7 @@
(run
ortac
qcheck-stm
%{dep:varray_circular_spec.mli}
%{dep:varray_circular_spec.gospel}
"make 42 'a'"
"char t"
--include=varray_incl
Expand Down
Loading

0 comments on commit d0a9a54

Please sign in to comment.