From 36264b8acbfdbc6fe6d84963d7a359f87b5849d5 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 19 Dec 2023 11:28:08 +0100 Subject: [PATCH 1/5] Move optional include argument in Registration The mechanism of including a module in the generated code will be common to several plugins. --- bin/registration.ml | 7 +++++++ bin/registration.mli | 1 + 2 files changed, 8 insertions(+) diff --git a/bin/registration.ml b/bin/registration.ml index 4babeab8..03954c7f 100644 --- a/bin/registration.ml +++ b/bin/registration.ml @@ -12,6 +12,13 @@ let setup_log = let init style_renderer = Fmt_tty.setup_std_outputs ?style_renderer () in Term.(const init $ Fmt_cli.style_renderer ()) +let include_ = + Arg.( + value + & opt (some string) None + & info [ "i"; "include" ] ~docv:"MODULE" + ~doc:"Include MODULE in the generated code.") + let output_file = let parse s = match Sys.is_directory s with diff --git a/bin/registration.mli b/bin/registration.mli index 9c027677..fbc7e8ee 100644 --- a/bin/registration.mli +++ b/bin/registration.mli @@ -5,6 +5,7 @@ val register : unit Cmdliner.Cmd.t -> unit val fold : ('a -> unit Cmdliner.Cmd.t -> 'a) -> 'a -> plugins -> 'a val get_out_formatter : string option -> Format.formatter val setup_log : unit Cmdliner.Term.t +val include_ : string option Cmdliner.Term.t val output_file : string option Cmdliner.Term.t val ocaml_file : string Cmdliner.Term.t val quiet : bool Cmdliner.Term.t From 12d0670512b3199dc43146e3135ea0f1251ac63f Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 5 Dec 2023 15:25:59 +0100 Subject: [PATCH 2/5] Add a dune plugin to generate dune rules This commit only propose the `qcheck-stm` sub-command as this is the only plugin release at the moment. --- dune-project | 15 ++ ortac-dune.opam | 35 +++++ plugins/dune | 1 + plugins/dune-rules/dune | 4 + plugins/dune-rules/src/dune | 11 ++ plugins/dune-rules/src/dune_rules.ml | 88 +++++++++++ plugins/dune-rules/src/qcheck_stm.ml | 163 +++++++++++++++++++++ plugins/dune-rules/src/qcheck_stm.mli | 11 ++ plugins/qcheck-stm/src/ortac_qcheck_stm.ml | 7 - 9 files changed, 328 insertions(+), 7 deletions(-) create mode 100644 ortac-dune.opam create mode 100644 plugins/dune-rules/dune create mode 100644 plugins/dune-rules/src/dune create mode 100644 plugins/dune-rules/src/dune_rules.ml create mode 100644 plugins/dune-rules/src/qcheck_stm.ml create mode 100644 plugins/dune-rules/src/qcheck_stm.mli diff --git a/dune-project b/dune-project index c10118b4..61ec6f7c 100644 --- a/dune-project +++ b/dune-project @@ -164,6 +164,21 @@ (conflicts (result (< 1.5)))) +; Dune plugin +(package + (name ortac-dune) + (synopsis "Generate dune rules for other ortac plugins") + (description "Generate dune rules for other ortac plugins") + (authors + "Nicolas Osborne ") + (maintainers "Nicolas Osborne ") + (depends + (ocaml (>= 4.11.0)) + fmt + (cmdliner (>= 1.1.0)) + ortac-core + (ortac-qcheck-stm :with-test))) + (package (name ortac-examples) (synopsis diff --git a/ortac-dune.opam b/ortac-dune.opam new file mode 100644 index 00000000..e401f71a --- /dev/null +++ b/ortac-dune.opam @@ -0,0 +1,35 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Generate dune rules for other ortac plugins" +description: "Generate dune rules for other ortac plugins" +maintainer: ["Nicolas Osborne "] +authors: ["Nicolas Osborne "] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.8"} + "ocaml" {>= "4.11.0"} + "fmt" + "cmdliner" {>= "1.1.0"} + "ortac-core" + "ortac-qcheck-stm" {with-test} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +dev-repo: "git+https://github.com/ocaml-gospel/ortac.git" diff --git a/plugins/dune b/plugins/dune index 7061e246..3664d847 100644 --- a/plugins/dune +++ b/plugins/dune @@ -3,4 +3,5 @@ (deps (alias monolith/default) (alias qcheck-stm/default) + (alias dune-rules/default) (alias wrapper/default))) diff --git a/plugins/dune-rules/dune b/plugins/dune-rules/dune new file mode 100644 index 00000000..b07b3872 --- /dev/null +++ b/plugins/dune-rules/dune @@ -0,0 +1,4 @@ +(alias + (name default) + (deps + (alias_rec src/default))) diff --git a/plugins/dune-rules/src/dune b/plugins/dune-rules/src/dune new file mode 100644 index 00000000..6a0f376e --- /dev/null +++ b/plugins/dune-rules/src/dune @@ -0,0 +1,11 @@ +(library + (public_name ortac-dune.plugin) + (name ortac_dune) + (libraries cmdliner fmt ortac-core.register)) + +(plugin + (name dune-rules) + (package ortac-dune) + (libraries ortac-dune.plugin) + (site + (ortac-core plugins))) diff --git a/plugins/dune-rules/src/dune_rules.ml b/plugins/dune-rules/src/dune_rules.ml new file mode 100644 index 00000000..dc278113 --- /dev/null +++ b/plugins/dune-rules/src/dune_rules.ml @@ -0,0 +1,88 @@ +open Cmdliner + +module Plugin : sig + val cmd : unit Cmd.t +end = struct + module Qcheck_stm : sig + val cmd : unit Cmd.t + end = struct + let info = + Cmd.info "qcheck-stm" + ~doc:"Generate Dune rules for the qcheck-stm plugin." + + let interface_file = + Arg.( + required + & pos 0 (some string) None + & info [] ~doc:"Interface file containing Gospel specifications" + ~docv:"INTERFACE") + + let init = + Arg.( + required + & pos 1 (some string) None + & info [] ~doc:"Init function to feed to ortac qcheck-stm" ~docv:"INIT") + + let sut = + Arg.( + required + & pos 2 (some string) None + & info [] ~doc:"Sut type to feed to ortac qcheck-stm" ~docv:"SUT") + + let ocaml_output = + Arg.( + required + & pos 3 (some string) None + & info [] ~doc:"Filename for the generated tests" ~docv:"OCAML_OUTPUT") + + let package_name = + Arg.( + value + & opt (some string) None + & info [ "p"; "package" ] ~doc:"Package name" ~docv:"PACKAGE") + + let with_stdout_to = + Arg.( + value + & opt (some string) None + & info [ "w"; "with-stdout-to" ] + ~doc:"Filename for the generated dune rules" ~docv:"DUNE_OUTPUT") + + let main interface_file init_function sut_type ocaml_output include_ + package_name dune_output = + let open Qcheck_stm in + let config = + { + interface_file; + init_function; + sut_type; + ocaml_output; + include_; + package_name; + dune_output; + } + in + let ppf = Registration.get_out_formatter dune_output in + Qcheck_stm.gen_dune_rules ppf config + + let term = + Term.( + const main + $ interface_file + $ init + $ sut + $ ocaml_output + $ Registration.include_ + $ package_name + $ with_stdout_to) + + let cmd = Cmd.v info term + end + + let cmd = + let info = Cmd.info "dune" ~doc:"Generate Dune rule for ortac plugins." in + Cmd.group info [ Qcheck_stm.cmd ] +end + +(* let () = Stdlib.exit (Cmd.eval Plugin.cmd) *) +let () = Registration.register Plugin.cmd diff --git a/plugins/dune-rules/src/qcheck_stm.ml b/plugins/dune-rules/src/qcheck_stm.ml new file mode 100644 index 00000000..3adf03b8 --- /dev/null +++ b/plugins/dune-rules/src/qcheck_stm.ml @@ -0,0 +1,163 @@ +type config = { + interface_file : string; + init_function : string; + sut_type : string; + ocaml_output : string; + include_ : string option; + package_name : string option; + dune_output : string option; +} + +type plugin = Dune | QCheckSTM + +open Fmt + +let msg ppf config = + pf ppf + "; This file is generated by ortac dune qcheck-stm@\n\ + ; It contains the rules for generating and running QCheck-STM tests for %s@\n\ + ; It also contains the rule to generate itself, so you can edit this rule \ + to@\n\ + ; change some options rather that running ortac on the command line again@\n" + config.interface_file + +let quote ppf s = pf ppf "%S" s +let stanza k ppf config = pf ppf "@[(%a)@]" k config +let stanza_rule k ppf config = pf ppf "%a@." (stanza k) config + +let with_target k ppf config = + let k ppf config = pf ppf "with-stdout-to@;%s@;%a" "%{targets}" k config in + stanza k ppf config + +let setenv v k ppf = + let k ppf config = pf ppf "setenv@;ORTAC_ONLY_PLUGIN@;%s@;%a" v k config in + stanza k ppf + +let action ppf k = + let k ppf config = pf ppf "action@;%a" k config in + stanza k ppf + +let action_with_env plug ppf k = + let v = match plug with Dune -> "dune-rules" | QCheckSTM -> "qcheck-stm" in + let k ppf = setenv v k ppf in + action ppf k + +let rule ppf stanzas = pf ppf "rule@;%a" (concat stanzas) +let test ppf stanzas = pf ppf "test@;%a" (concat stanzas) +let run ppf args = pf ppf "run@;%a" (concat args) +let ortac ppf _ = pf ppf "ortac" +let dune ppf _ = pf ppf "dune" +let qcheck_stm ppf _ = pf ppf "qcheck-stm" +let interface ppf config = pf ppf "%s" config.interface_file +let interface_mli ppf config = pf ppf "%%{dep:%s.mli}" config.interface_file +let init_sut ppf config = pf ppf "%a" quote config.init_function +let sut ppf config = pf ppf "%a" quote config.sut_type +let ocaml_output ppf config = pf ppf "%s" config.ocaml_output +let runtest ppf _ = pf ppf "(alias runtest)" +let promote ppf _ = pf ppf "(mode promote)" +let name ppf config = pf ppf "(name %s)" config.ocaml_output + +let libraries = + let k ppf config = + pf ppf + "libraries@ %s@ qcheck-stm.stm@ qcheck-stm.sequential@ \ + qcheck-multicoretests-util@ ortac-runtime" + config.interface_file + in + stanza k + +let deps plug ppf _ = + let p = + match plug with Dune -> "ortac-dune" | QCheckSTM -> "ortac-qcheck-stm" + in + let package = + let aux ppf = pf ppf "package %s" in + stanza aux + in + pf ppf "(deps@; %a)" package p + +let optional ppf s = function None -> () | Some x -> pf ppf s x +let include_ ppf config = optional ppf "--include=%s" config.include_ +let quiet ppf _ = pf ppf "--quiet" +let package_opt ppf config = optional ppf "--package=%s" config.package_name +let package ppf config = optional ppf "(package %s)" config.package_name +let targets_ml ppf config = pf ppf "(targets %s.ml)" config.ocaml_output +let targets_dune ppf config = optional ppf "(targets %s)" config.dune_output + +let with_stdout_to ppf config = + optional ppf "--with-stdout-to=%s" config.dune_output + +type optional_stanza = + | Include_ + | Package_opt + | Package + | Targets_dune + | With_stdout_to + +let get config = + let aux x = function None -> [] | Some _ -> [ x ] in + function + | Include_ -> aux include_ config.include_ + | Package_opt -> aux package_opt config.package_name + | Package -> aux package config.package_name + | Targets_dune -> aux targets_dune config.dune_output + | With_stdout_to -> aux with_stdout_to config.dune_output + +let gen_gen_rule ppf config = + let get = get config in + let opt_args = + List.flatten [ get Include_; get Package_opt; get With_stdout_to ] + in + let args = + [ ortac; dune; qcheck_stm; interface; init_sut; sut; ocaml_output ] + @ opt_args + in + let run ppf = run ppf args in + let run = stanza run in + let action ppf config = action_with_env Dune ppf run config in + let opt_stanzas = List.flatten [ get Package; get Targets_dune ] in + let stanzas = [ runtest; promote; deps Dune ] @ opt_stanzas @ [ action ] in + let rule ppf = rule ppf stanzas in + stanza_rule rule ppf config + +let gen_ortac_rule ppf config = + let get = get config in + let args = + [ ortac; qcheck_stm; interface_mli; init_sut; sut ] + @ get Include_ + @ [ quiet ] + in + let run ppf = run ppf args in + let run = stanza run in + let action ppf = action_with_env QCheckSTM ppf (with_target run) in + let stanzas = + [ runtest; promote ] @ get Package @ [ deps QCheckSTM; targets_ml; action ] + in + let rule ppf = rule ppf stanzas in + stanza_rule rule ppf config + +let gen_test_rule ppf config = + let get = get config in + let modules ppf config = + match config.include_ with + | None -> pf ppf "(modules %s)" config.ocaml_output + | Some i -> pf ppf "(modules %s %s)" config.ocaml_output i + in + let run ppf = + run ppf + [ + (fun ppf _ -> pf ppf "%s" "%{test}"); (fun ppf _ -> pf ppf "--verbose"); + ] + in + let action ppf = action ppf (stanza run) in + let test ppf = + test ppf ([ name; modules; libraries ] @ get Package @ [ action ]) + in + stanza_rule test ppf config + +let gen_dune_rules ppf config = + let rules = [ gen_gen_rule; gen_ortac_rule; gen_test_rule ] in + let rules = + if Option.is_some config.dune_output then msg :: rules else rules + in + concat ~sep:cut rules ppf config diff --git a/plugins/dune-rules/src/qcheck_stm.mli b/plugins/dune-rules/src/qcheck_stm.mli new file mode 100644 index 00000000..e9e3e189 --- /dev/null +++ b/plugins/dune-rules/src/qcheck_stm.mli @@ -0,0 +1,11 @@ +type config = { + interface_file : string; + init_function : string; + sut_type : string; + ocaml_output : string; + include_ : string option; + package_name : string option; + dune_output : string option; +} + +val gen_dune_rules : config Fmt.t diff --git a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml index eac712ab..345d4fd0 100644 --- a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml +++ b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml @@ -38,13 +38,6 @@ end = struct system under test." ~docv:"INIT") - let include_ = - Arg.( - value - & opt (some string) None - & info [ "i"; "include" ] ~docv:"MODULE" - ~doc:"Include MODULE in the generated code.") - let term = let open Registration in Term.( From 79dc3e99e48958165b439266b72c1fbca4cd0db3 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Mon, 18 Dec 2023 10:08:51 +0100 Subject: [PATCH 3/5] Add a cram test --- plugins/dune-rules/test/dune | 6 ++ plugins/dune-rules/test/test.t | 135 +++++++++++++++++++++++++++++++++ 2 files changed, 141 insertions(+) create mode 100644 plugins/dune-rules/test/dune create mode 100644 plugins/dune-rules/test/test.t diff --git a/plugins/dune-rules/test/dune b/plugins/dune-rules/test/dune new file mode 100644 index 00000000..2fc59f68 --- /dev/null +++ b/plugins/dune-rules/test/dune @@ -0,0 +1,6 @@ +(cram + (package ortac-dune) + (deps + (package ortac-core) + (package ortac-qcheck-stm) + (package ortac-dune))) diff --git a/plugins/dune-rules/test/test.t b/plugins/dune-rules/test/test.t new file mode 100644 index 00000000..289d7bc7 --- /dev/null +++ b/plugins/dune-rules/test/test.t @@ -0,0 +1,135 @@ +This file test the behaviour of the `qcheck-stm` sub-command of the `dune` plugin. + +$ export ORTAC_ONLY_PLUGIN=dune-rules + +Without the optional output argument (for the dune rules, output for the generated OCaml +have to be set), the rules are printed on stdout. This is useful to check what will be +generated. + $ ortac dune qcheck-stm intf_spec "init_sut ()" "int sut" test --include=included --package=my_package + (rule + (alias runtest) + (mode promote) + (deps + (package ortac-dune)) + (package my_package) + (action + (setenv + ORTAC_ONLY_PLUGIN + dune-rules + (run + ortac + dune + qcheck-stm + intf_spec + "init_sut ()" + "int sut" + test + --include=included + --package=my_package)))) + + (rule + (alias runtest) + (mode promote) + (package my_package) + (deps + (package ortac-qcheck-stm)) + (targets test.ml) + (action + (setenv + ORTAC_ONLY_PLUGIN + qcheck-stm + (with-stdout-to + %{targets} + (run + ortac + qcheck-stm + %{dep:intf_spec.mli} + "init_sut ()" + "int sut" + --include=included + --quiet))))) + + (test + (name test) + (modules test included) + (libraries + intf_spec + qcheck-stm.stm + qcheck-stm.sequential + qcheck-multicoretests-util + ortac-runtime) + (package my_package) + (action + (run + %{test} + --verbose))) + +When the optional output argument is set, rules will be written in the file and will reflect +this fact. + + $ ortac dune qcheck-stm intf_spec "init_sut ()" "int sut" test --include=included --package=my_package --with-stdout-to=dune.inc + $ cat dune.inc + ; This file is generated by ortac dune qcheck-stm + ; It contains the rules for generating and running QCheck-STM tests for intf_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 my_package) + (targets dune.inc) + (action + (setenv + ORTAC_ONLY_PLUGIN + dune-rules + (run + ortac + dune + qcheck-stm + intf_spec + "init_sut ()" + "int sut" + test + --include=included + --package=my_package + --with-stdout-to=dune.inc)))) + + (rule + (alias runtest) + (mode promote) + (package my_package) + (deps + (package ortac-qcheck-stm)) + (targets test.ml) + (action + (setenv + ORTAC_ONLY_PLUGIN + qcheck-stm + (with-stdout-to + %{targets} + (run + ortac + qcheck-stm + %{dep:intf_spec.mli} + "init_sut ()" + "int sut" + --include=included + --quiet))))) + + (test + (name test) + (modules test included) + (libraries + intf_spec + qcheck-stm.stm + qcheck-stm.sequential + qcheck-multicoretests-util + ortac-runtime) + (package my_package) + (action + (run + %{test} + --verbose))) From 4b68edffec2e848da2b9f2a2fb81f6915a1290b3 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Mon, 15 Jan 2024 17:07:14 +0100 Subject: [PATCH 4/5] Use Ortac/Dune in examples package --- dune-project | 1 + examples/README.md | 19 ++++- examples/dune | 114 +----------------------------- examples/dune.lwt_dllist.inc | 64 +++++++++++++++++ examples/dune.varray.inc | 64 +++++++++++++++++ examples/dune.varray_circular.inc | 64 +++++++++++++++++ examples/varray_circular_incl.ml | 27 +++++++ examples/varray_circular_tests.ml | 2 +- ortac-examples.opam | 1 + 9 files changed, 243 insertions(+), 113 deletions(-) create mode 100644 examples/dune.lwt_dllist.inc create mode 100644 examples/dune.varray.inc create mode 100644 examples/dune.varray_circular.inc create mode 100644 examples/varray_circular_incl.ml diff --git a/dune-project b/dune-project index 61ec6f7c..6b2091d4 100644 --- a/dune-project +++ b/dune-project @@ -191,6 +191,7 @@ (ocaml (>= 4.11.0)) ortac-core ortac-qcheck-stm + ortac-dune ortac-runtime qcheck-stm lwt-dllist diff --git a/examples/README.md b/examples/README.md index 1ae96cbc..24239c70 100644 --- a/examples/README.md +++ b/examples/README.md @@ -36,6 +36,13 @@ The generated code can be found in `lwt_dllist_tests.ml`. You can run the test either with `dune runtest examples/` or by directly running the compiled executable that you will find in your `_build` directory. +Dune rules have been generated using the `dune-rules` plugin, providing the +`dune` subcommand: + +```sh +$ 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 +``` + ## `varray` library This is an example of a library exposing a Functor. In order to test a Functor, @@ -55,8 +62,18 @@ dune-generated `mli` files hidden in the `_build` folder. Here again, as for the previous example, we need to include some code. That is the extension of the `STM.ty` type. But also a `QCheck` generator for the `'a elt` type, as some functions of the library take arguments of this type. You -can find these extensions in the `varray_incl.ml` file. +can find these extensions in the `varray_incl.ml` and `varray_circular_incl.ml` +files. The generated code can be found in the respective `varray*tests.ml` files. They have been promoted in the source tree in order to be easily accessible for reading and curiosity purposes, but this is not necessary for testing purposes. + +Dune rules have been generated again using the `dune-rules` plugin with the +following command for `varray_spec.mli` and an adapted version for +`varray_circular_spec.mli`: + +```sh +$ 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 +``` + diff --git a/examples/dune b/examples/dune index f6c235dd..fc21a4a9 100644 --- a/examples/dune +++ b/examples/dune @@ -8,45 +8,7 @@ (:standard -w -69)) (package ortac-examples)) -(rule - (alias runtest) - (mode promote) - (package ortac-examples) - (deps - (package ortac-qcheck-stm) - lwt_dllist_incl.ml) - (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 - ortac-runtime) - (package ortac-examples) - (action - (run %{test} --verbose))) - -(library - (name varray_incl) - (modules varray_incl) - (libraries qcheck-stm.sequential qcheck-multicoretests-util varray_spec)) +(include dune.lwt_dllist.inc) (rule (enabled_if %{bin-available:awk}) @@ -67,42 +29,7 @@ (libraries varray) (package ortac-examples)) -(rule - (mode promote) - (alias runtest) - (package ortac-examples) - (deps - (package ortac-qcheck-stm) - varray_incl.ml) - (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) - (libraries - varray_incl - varray_spec - qcheck-stm.stm - qcheck-stm.sequential - qcheck-multicoretests-util - ortac-runtime) - (package ortac-examples) - (action - (run %{test} --verbose))) +(include dune.varray.inc) (rule (copy varray_spec.mli varray_circular_spec.mli)) @@ -113,39 +40,4 @@ (libraries varray) (package ortac-examples)) -(rule - (mode promote) - (alias runtest) - (package ortac-examples) - (deps - (package ortac-qcheck-stm) - varray_incl.ml) - (targets varray_circular_tests.ml) - (action - (setenv - ORTAC_ONLY_PLUGIN - qcheck-stm - (with-stdout-to - %{targets} - (run - ortac - qcheck-stm - %{dep:varray_circular_spec.mli} - "make 42 'a'" - "char t" - --include=varray_incl - --quiet))))) - -(test - (name varray_circular_tests) - (modules varray_circular_tests) - (libraries - varray_incl - varray_circular_spec - qcheck-stm.stm - qcheck-stm.sequential - qcheck-multicoretests-util - ortac-runtime) - (package ortac-examples) - (action - (run %{test} --verbose))) +(include dune.varray_circular.inc) diff --git a/examples/dune.lwt_dllist.inc b/examples/dune.lwt_dllist.inc new file mode 100644 index 00000000..1388a7cf --- /dev/null +++ b/examples/dune.lwt_dllist.inc @@ -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))) diff --git a/examples/dune.varray.inc b/examples/dune.varray.inc new file mode 100644 index 00000000..e9ccbd83 --- /dev/null +++ b/examples/dune.varray.inc @@ -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))) diff --git a/examples/dune.varray_circular.inc b/examples/dune.varray_circular.inc new file mode 100644 index 00000000..e84c9e0b --- /dev/null +++ b/examples/dune.varray_circular.inc @@ -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_circular_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_circular.inc) + (action + (setenv + ORTAC_ONLY_PLUGIN + dune-rules + (run + ortac + dune + qcheck-stm + varray_circular_spec + "make 42 'a'" + "char t" + varray_circular_tests + --include=varray_circular_incl + --package=ortac-examples + --with-stdout-to=dune.varray_circular.inc)))) + +(rule + (alias runtest) + (mode promote) + (package ortac-examples) + (deps + (package ortac-qcheck-stm)) + (targets varray_circular_tests.ml) + (action + (setenv + ORTAC_ONLY_PLUGIN + qcheck-stm + (with-stdout-to + %{targets} + (run + ortac + qcheck-stm + %{dep:varray_circular_spec.mli} + "make 42 'a'" + "char t" + --include=varray_circular_incl + --quiet))))) + +(test + (name varray_circular_tests) + (modules varray_circular_tests varray_circular_incl) + (libraries + varray_circular_spec + qcheck-stm.stm + qcheck-stm.sequential + qcheck-multicoretests-util + ortac-runtime) + (package ortac-examples) + (action + (run + %{test} + --verbose))) diff --git a/examples/varray_circular_incl.ml b/examples/varray_circular_incl.ml new file mode 100644 index 00000000..cfe35125 --- /dev/null +++ b/examples/varray_circular_incl.ml @@ -0,0 +1,27 @@ +module Util = struct + module Pp = struct + include Util.Pp + + let pp_elt pp = pp + end +end + +module QCheck = struct + include QCheck + + module Gen = struct + include QCheck.Gen + + let int = small_signed_int + let elt gen = gen + end +end + +open STM +open Varray_circular_spec + +type _ ty += Elt : 'a ty -> 'a elt ty + +let elt spec = + let ty, show = spec in + (Elt ty, fun x -> Printf.sprintf "Elt %s" (show x)) diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml index 550c60d8..eaf06d96 100644 --- a/examples/varray_circular_tests.ml +++ b/examples/varray_circular_tests.ml @@ -59,7 +59,7 @@ module Spec = struct open STM [@@@ocaml.warning "-26-27"] - include Varray_incl + include Varray_circular_incl type sut = char t type cmd = | Push_back of char elt diff --git a/ortac-examples.opam b/ortac-examples.opam index 3d2d55ee..f28c6bfc 100644 --- a/ortac-examples.opam +++ b/ortac-examples.opam @@ -14,6 +14,7 @@ depends: [ "ocaml" {>= "4.11.0"} "ortac-core" "ortac-qcheck-stm" + "ortac-dune" "ortac-runtime" "qcheck-stm" "lwt-dllist" From 784aa03b26de7715e6c7a7bd2e7afaf562ed051a Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 16 Jan 2024 11:30:39 +0100 Subject: [PATCH 5/5] Update Changelog and add README --- README.md | 1 + plugins/dune-rules/README.md | 40 ++++++++++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+) create mode 100644 plugins/dune-rules/README.md diff --git a/README.md b/README.md index dc3cca29..c7845a8b 100644 --- a/README.md +++ b/README.md @@ -70,6 +70,7 @@ _experimental_ packages: `ortac` command-line tool, - `ortac-runtime-monolith.opam` which provides the support library for the code generated with the Monolith plugin. +- `ortac-dune.opam` which provides a dune rule generator. Even using `opam pin`, you can install only some of those packages by explicitly mentioning which package you want to install, for instance: diff --git a/plugins/dune-rules/README.md b/plugins/dune-rules/README.md new file mode 100644 index 00000000..f0901e19 --- /dev/null +++ b/plugins/dune-rules/README.md @@ -0,0 +1,40 @@ +# Dune-rules plugin for Ortac + +This directory contains a plugin for [Ortac] that can generate the dune rules +for the other plugins. + +[Ortac]: ../../README.md + +## Installation + +Follow the global [installation instructions] in the main README of +this repository. The dune-rules plugin is provided by the OPAM package +`ortac-dune.opam`. + +[installation instructions]: ../../README.md#installation + +## Quick start + +The dune-rules plugin can be used to generate dune rules for other ortac +plugins (the qcheck-stm plugin for now). You have to give it the option you want to +pass to the other plugins and some more information for dune. + +Let's say you want use the [Ortac/QCheck-STM] plugin on a module interface +`lib.mli` to generate QCheck-STM tests for this module using `make 42 'a'` as +initial value of type `char t`, including the `Lib_incl` module, in the context +of the `pack` package. + +Then you can run: + +```shell +$ ortac dune qcheck-stm lib "make 42 'a'" "char t" lib_tests --include=lib_incl --package=pack --with-stdout-to=dune.inc +``` + +to generate the dune rules to generate and run the tests. Next time you run +`dune runtest`, your code should be tested using QCheck-STM. + +[Ortac/QCheck-STM]: ../qcheck-stm/README.md + +## Supported plugins + +- `qcheck-stm`