From 6910facf56cd8b36f7b7cc7bb099cf961628ea3b Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Thu, 19 Mar 2026 15:11:39 +0100 Subject: [PATCH] [new release] Ortac 0.8.0 This release brings the possibility of generating QCheck-STM+Domains tests. The main issues were to handle the SUTs created during the run of the generated programs and to adapt the bug report feature to parallel programs. This adds a new `ortac_runtime_qcheck_stm_domain` library, that is enabled only if ocaml version is at least 5. Other changes: - Fix field access in check clauses in wrapper plugin - Add optional argument to control aliases in dune plugin - Add a count argument to `ortac qcheck-stm` and `ortac dune qcheck-stm` - Update to QCheck 0.90 great renaming - Allow user to provide weight per command and per program sub-part in Ortac/QCheck-STM configuration file, to be used in the generated command generator - Allow user to provide complete custom command generators in Ortac/QCheck-STM configuration file - Add some new examples and tests to demonstrate testing in a parallel context --- packages/ortac-core/ortac-core.0.8.0/opam | 65 +++++++++++++++++++ packages/ortac-dune/ortac-dune.0.8.0/opam | 47 ++++++++++++++ .../ortac-qcheck-stm.0.8.0/opam | 64 ++++++++++++++++++ .../ortac-runtime-qcheck-stm.0.8.0/opam | 51 +++++++++++++++ .../ortac-runtime/ortac-runtime.0.8.0/opam | 52 +++++++++++++++ .../ortac-wrapper/ortac-wrapper.0.8.0/opam | 57 ++++++++++++++++ 6 files changed, 336 insertions(+) create mode 100644 packages/ortac-core/ortac-core.0.8.0/opam create mode 100644 packages/ortac-dune/ortac-dune.0.8.0/opam create mode 100644 packages/ortac-qcheck-stm/ortac-qcheck-stm.0.8.0/opam create mode 100644 packages/ortac-runtime-qcheck-stm/ortac-runtime-qcheck-stm.0.8.0/opam create mode 100644 packages/ortac-runtime/ortac-runtime.0.8.0/opam create mode 100644 packages/ortac-wrapper/ortac-wrapper.0.8.0/opam diff --git a/packages/ortac-core/ortac-core.0.8.0/opam b/packages/ortac-core/ortac-core.0.8.0/opam new file mode 100644 index 000000000000..87943925e99e --- /dev/null +++ b/packages/ortac-core/ortac-core.0.8.0/opam @@ -0,0 +1,65 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: + "Ortac (OCaml Runtime Assertion Checking) core tool and library based on Gospel" +description: """ +Ortac (OCaml Runtime Assertion Checking) is a tool to turn +executable Gospel specifications into code to test they hold. +Ortac Core provides: +- a library to turn Gospel terms and types into OCaml expressions + and types, +- and a command-line tool. +You will need at least one of the Ortac plugins to actually +generate test code. +""" +maintainer: ["Nicolas Osborne "] +authors: [ + "Clément Pascutto " + "Nicolas Osborne " + "Samuel Hym " +] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +doc: "https://ocaml-gospel.github.io/ortac/ortac-core/" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.9"} + "ocaml" {>= "4.12.0"} + "dune-build-info" + "dune-site" + "cmdliner" {>= "1.3.0"} + "fmt" + "ppxlib" {>= "0.36.0"} + "gospel" {= "0.3.1"} + "alcotest" {with-test & >= "0.8.1"} + "ortac-runtime" {with-test & = version} + "odoc" {with-doc} +] +conflicts: [ + "result" {< "1.5"} +] +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" +x-maintenance-intent: ["(latest)"] +url { + src: "https://github.com/ocaml-gospel/ortac/archive/refs/tags/0.8.0/.tar.gz" + checksum: [ + "md5=1bef0290fc0c4d00fcf3b7d40e47650f" + "sha512=57982ebdd63a30237a8f334246f1cf977614b75aecd60659fb925c41887d744fef2cdc45e38466e0ab2e8701801c14831e6afd69780bec88848b154e32fc70a6" + ] +} diff --git a/packages/ortac-dune/ortac-dune.0.8.0/opam b/packages/ortac-dune/ortac-dune.0.8.0/opam new file mode 100644 index 000000000000..661609644c99 --- /dev/null +++ b/packages/ortac-dune/ortac-dune.0.8.0/opam @@ -0,0 +1,47 @@ +# 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 " + "Charlène Gros " +] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.9"} + "ocaml" {>= "4.12.0"} + "fmt" + "cmdliner" {>= "1.3.0"} + "ortac-core" {= version} + "ortac-qcheck-stm" {with-test & = version} + "ortac-wrapper" {with-test & = version} + "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" +x-maintenance-intent: ["(latest)"] +url { + src: "https://github.com/ocaml-gospel/ortac/archive/refs/tags/0.8.0/.tar.gz" + checksum: [ + "md5=1bef0290fc0c4d00fcf3b7d40e47650f" + "sha512=57982ebdd63a30237a8f334246f1cf977614b75aecd60659fb925c41887d744fef2cdc45e38466e0ab2e8701801c14831e6afd69780bec88848b154e32fc70a6" + ] +} diff --git a/packages/ortac-qcheck-stm/ortac-qcheck-stm.0.8.0/opam b/packages/ortac-qcheck-stm/ortac-qcheck-stm.0.8.0/opam new file mode 100644 index 000000000000..6f7a444e1692 --- /dev/null +++ b/packages/ortac-qcheck-stm/ortac-qcheck-stm.0.8.0/opam @@ -0,0 +1,64 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "QCheck-STM plugin for Ortac" +description: """ +The QCheck-STM plugin for the Ortac command-line tool (provided by +the ortac-core package) can generate model-based tests for a module +with Gospel specifications. The generated code will test that the +function specifications hold by using the QCheck-STM library to +create random test cases. + +Ortac (OCaml Runtime Assertion Checking) is a tool to turn +executable Gospel specifications into code to test they hold. +""" +maintainer: ["Nicolas Osborne "] +authors: [ + "Nicolas Osborne " + "Samuel Hym " + "Nikolaus Huber " +] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +doc: "https://ocaml-gospel.github.io/ortac/ortac-qcheck-stm/" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.9"} + "ocaml" {>= "4.12.0"} + "cmdliner" {>= "1.3.0"} + "fmt" + "ppxlib" {>= "0.36.0"} + "mdx" {with-test & >= "2.3.0"} + "gospel" {= "0.3.1"} + "qcheck-stm" {>= "0.5"} + "ortac-core" {= version} + "ortac-runtime-qcheck-stm" {= version} + "odoc" {with-doc} +] +conflicts: [ + "result" {< "1.5"} +] +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" +x-maintenance-intent: ["(latest)"] +url { + src: "https://github.com/ocaml-gospel/ortac/archive/refs/tags/0.8.0/.tar.gz" + checksum: [ + "md5=1bef0290fc0c4d00fcf3b7d40e47650f" + "sha512=57982ebdd63a30237a8f334246f1cf977614b75aecd60659fb925c41887d744fef2cdc45e38466e0ab2e8701801c14831e6afd69780bec88848b154e32fc70a6" + ] +} diff --git a/packages/ortac-runtime-qcheck-stm/ortac-runtime-qcheck-stm.0.8.0/opam b/packages/ortac-runtime-qcheck-stm/ortac-runtime-qcheck-stm.0.8.0/opam new file mode 100644 index 000000000000..60a15bf73584 --- /dev/null +++ b/packages/ortac-runtime-qcheck-stm/ortac-runtime-qcheck-stm.0.8.0/opam @@ -0,0 +1,51 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Runtime support library for Ortac/QCheck-STM-generated code" +description: """ +The ortac-runtime-qcheck-stm library provides support for the code +generated by the Ortac/QCheck-STM plugin (provided by the +ortac-qcheck-stm package). + +Ortac (OCaml Runtime Assertion Checking) is a tool to turn +executable Gospel specifications into code to test they hold. +""" +maintainer: ["Nicolas Osborne "] +authors: [ + "Nicolas Osborne " + "Nikolaus Huber " +] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.9"} + "ocaml" {>= "4.12.0"} + "qcheck-stm" {>= "0.5"} + "ortac-runtime" {= version} + "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" +x-maintenance-intent: ["(latest)"] +url { + src: "https://github.com/ocaml-gospel/ortac/archive/refs/tags/0.8.0/.tar.gz" + checksum: [ + "md5=1bef0290fc0c4d00fcf3b7d40e47650f" + "sha512=57982ebdd63a30237a8f334246f1cf977614b75aecd60659fb925c41887d744fef2cdc45e38466e0ab2e8701801c14831e6afd69780bec88848b154e32fc70a6" + ] +} diff --git a/packages/ortac-runtime/ortac-runtime.0.8.0/opam b/packages/ortac-runtime/ortac-runtime.0.8.0/opam new file mode 100644 index 000000000000..8b9012e0c6b8 --- /dev/null +++ b/packages/ortac-runtime/ortac-runtime.0.8.0/opam @@ -0,0 +1,52 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Runtime support library for Ortac-generated code" +description: """ +The ortac-runtime library provides support for the code generated +by the various Ortac plugins. +Ortac (OCaml Runtime Assertion Checking) is a tool to turn +executable Gospel specifications into code to test they hold. +""" +maintainer: ["Nicolas Osborne "] +authors: [ + "Clément Pascutto " + "Nicolas Osborne " + "Samuel Hym " +] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +doc: "https://ocaml-gospel.github.io/ortac/ortac-runtime/" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.9"} + "ocaml" {>= "4.12.0"} + "fmt" {>= "0.8.7"} + "zarith" + "monolith" {with-test & >= "20201026"} + "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" +x-maintenance-intent: ["(latest)"] +url { + src: "https://github.com/ocaml-gospel/ortac/archive/refs/tags/0.8.0/.tar.gz" + checksum: [ + "md5=1bef0290fc0c4d00fcf3b7d40e47650f" + "sha512=57982ebdd63a30237a8f334246f1cf977614b75aecd60659fb925c41887d744fef2cdc45e38466e0ab2e8701801c14831e6afd69780bec88848b154e32fc70a6" + ] +} diff --git a/packages/ortac-wrapper/ortac-wrapper.0.8.0/opam b/packages/ortac-wrapper/ortac-wrapper.0.8.0/opam new file mode 100644 index 000000000000..aaab474617d5 --- /dev/null +++ b/packages/ortac-wrapper/ortac-wrapper.0.8.0/opam @@ -0,0 +1,57 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Wrapper plugin for Ortac" +description: """ +The Wrapper plugin for the Ortac command-line tool (provided by the +ortac-core package) can generate a wrapper module, ie a module that +will wrap all function calls with runtime assertion checks that +their specifications hold. +Ortac (OCaml Runtime Assertion Checking) is a tool to turn +executable Gospel specifications into code to test they hold. +""" +maintainer: ["Nicolas Osborne "] +authors: [ + "Clément Pascutto " + "Nicolas Osborne " + "Charlène Gros " +] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.9"} + "ocaml" {>= "4.12.0"} + "cmdliner" {>= "1.3.0"} + "fmt" + "ppxlib" {>= "0.36.0"} + "gospel" {= "0.3.1"} + "alcotest" {with-test & >= "0.8.1"} + "ortac-core" {= version} + "ortac-runtime" {= version} + "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" +x-maintenance-intent: ["(latest)"] +url { + src: "https://github.com/ocaml-gospel/ortac/archive/refs/tags/0.8.0/.tar.gz" + checksum: [ + "md5=1bef0290fc0c4d00fcf3b7d40e47650f" + "sha512=57982ebdd63a30237a8f334246f1cf977614b75aecd60659fb925c41887d744fef2cdc45e38466e0ab2e8701801c14831e6afd69780bec88848b154e32fc70a6" + ] +}