forked from ocaml-gospel/ortac
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request ocaml-gospel#190 from n-osborne/ortac-dune
ortac-dune plugin
- Loading branch information
Showing
23 changed files
with
761 additions
and
120 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
; This file is generated by ortac dune qcheck-stm | ||
; It contains the rules for generating and running QCheck-STM tests for lwt_dllist_spec | ||
; It also contains the rule to generate itself, so you can edit this rule to | ||
; change some options rather that running ortac on the command line again | ||
|
||
(rule | ||
(alias runtest) | ||
(mode promote) | ||
(deps | ||
(package ortac-dune)) | ||
(package ortac-examples) | ||
(targets dune.lwt_dllist.inc) | ||
(action | ||
(setenv | ||
ORTAC_ONLY_PLUGIN | ||
dune-rules | ||
(run | ||
ortac | ||
dune | ||
qcheck-stm | ||
lwt_dllist_spec | ||
"create ()" | ||
"int t" | ||
lwt_dllist_tests | ||
--include=lwt_dllist_incl | ||
--package=ortac-examples | ||
--with-stdout-to=dune.lwt_dllist.inc)))) | ||
|
||
(rule | ||
(alias runtest) | ||
(mode promote) | ||
(package ortac-examples) | ||
(deps | ||
(package ortac-qcheck-stm)) | ||
(targets lwt_dllist_tests.ml) | ||
(action | ||
(setenv | ||
ORTAC_ONLY_PLUGIN | ||
qcheck-stm | ||
(with-stdout-to | ||
%{targets} | ||
(run | ||
ortac | ||
qcheck-stm | ||
%{dep:lwt_dllist_spec.mli} | ||
"create ()" | ||
"int t" | ||
--include=lwt_dllist_incl | ||
--quiet))))) | ||
|
||
(test | ||
(name lwt_dllist_tests) | ||
(modules lwt_dllist_tests lwt_dllist_incl) | ||
(libraries | ||
lwt_dllist_spec | ||
qcheck-stm.stm | ||
qcheck-stm.sequential | ||
qcheck-multicoretests-util | ||
ortac-runtime) | ||
(package ortac-examples) | ||
(action | ||
(run | ||
%{test} | ||
--verbose))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
; This file is generated by ortac dune qcheck-stm | ||
; It contains the rules for generating and running QCheck-STM tests for varray_spec | ||
; It also contains the rule to generate itself, so you can edit this rule to | ||
; change some options rather that running ortac on the command line again | ||
|
||
(rule | ||
(alias runtest) | ||
(mode promote) | ||
(deps | ||
(package ortac-dune)) | ||
(package ortac-examples) | ||
(targets dune.varray.inc) | ||
(action | ||
(setenv | ||
ORTAC_ONLY_PLUGIN | ||
dune-rules | ||
(run | ||
ortac | ||
dune | ||
qcheck-stm | ||
varray_spec | ||
"make 42 'a'" | ||
"char t" | ||
varray_tests | ||
--include=varray_incl | ||
--package=ortac-examples | ||
--with-stdout-to=dune.varray.inc)))) | ||
|
||
(rule | ||
(alias runtest) | ||
(mode promote) | ||
(package ortac-examples) | ||
(deps | ||
(package ortac-qcheck-stm)) | ||
(targets varray_tests.ml) | ||
(action | ||
(setenv | ||
ORTAC_ONLY_PLUGIN | ||
qcheck-stm | ||
(with-stdout-to | ||
%{targets} | ||
(run | ||
ortac | ||
qcheck-stm | ||
%{dep:varray_spec.mli} | ||
"make 42 'a'" | ||
"char t" | ||
--include=varray_incl | ||
--quiet))))) | ||
|
||
(test | ||
(name varray_tests) | ||
(modules varray_tests varray_incl) | ||
(libraries | ||
varray_spec | ||
qcheck-stm.stm | ||
qcheck-stm.sequential | ||
qcheck-multicoretests-util | ||
ortac-runtime) | ||
(package ortac-examples) | ||
(action | ||
(run | ||
%{test} | ||
--verbose))) |
Oops, something went wrong.