Getting Started Documentation

Organisations ocaml-gospel ortac branch/main Build History

Build History for branch/main

Builds (102)

Merge pull request #329 from n-osborne/dune-rules-qcheck-stm-domain This PR adds support for generating the dune rules for Ortac/QCheck-STM+Domain. The `ortac dune` cli command uses the same flag `--domain` as the `ortac qcheck-stm` one. This will pass the flag to the call to `ortac qcheck-stm` and adapt the dependencies accordingly.

Aug 28 15:48 +00:00

Failed in 52m35s

Merge pull request #328 from n-osborne/qcheck-stm-domain-runtime Merge pull request #328 from n-osborne:qcheck-stm-domain-runtime This PR add a basic runtime for QCheck-STM+Domains. A `--domain` flag is added to the cli tool. The default is then the generation of sequential testing. The command to generate QCheck-STM+Domains tests is: ``` $ ortac qcheck-stm interface.mli config.ml --domain ``` The runtime is basic in the sense that it comes with two limitations. The first one is that the runtime doesn't yet generate a bug report (like the one generated by the tests in a sequential context). The output in case of test failure is the original one from the QCheck-STM test framework. The second one is that we don't store the new SUTs created during the tests (by SUT-returning functions) in the store. This has the consequence of weakening the tests compared to the ones generated for the sequential context. The rational here is based on ease of implementation. Storing the newly created SUTs indeed implies to be able to differentiate between commands coming from the sequential prefix and the ones coming from one of the two parallel tails.

Aug 27 16:19 +00:00

Passed in 9m16s

Merge pull request #316 from n-osborne/refactor-ortac-runtime-qcheck-stm [QCheck-STM] Refactor runtime to allow for OCaml5-only sub-library

Aug 27 13:13 +00:00

Merge pull request #349 from Lucccyo/prepare_release_0.7.2 Prepare release 0.7.2

Aug 27 08:03 +00:00

Passed in 26m52s

Merge pull request #348 from Lucccyo/fix_cycle_dep Fix cycle dependency in `Ortac/Dune-rules` for wrapper plugin

Aug 26 14:45 +00:00

Passed in 12m44s

Merge pull request #352 from n-osborne/bump-monolith-plugin-version Bump version in *monolith.opam

Aug 26 13:59 +00:00

Failed in 44m18s

Merge pull request #344 from ocaml-gospel/revert-341-tmp_rm_ortac_monolith Revert "Remove Ortac/Monolith plugin temporarily"

Jul 31 07:28 +00:00

Failed in 3m44s

Merge pull request #343 from Lucccyo/prepare_release_0.7.1 Prepare release 0.7.1

Jul 11 07:34 +00:00

Passed in 3m14s

Merge pull request #341 from Lucccyo/tmp_rm_ortac_monolith Remove Ortac/Monolith plugin temporarily

Jul 10 10:07 +00:00

Passed in 5m43s

Merge pull request #342 from Lucccyo/update_rules Fix dependencies in generated library declaration for Ortac/Wrapper

Jul 10 09:59 +00:00

Passed in 1m20s

Merge pull request #340 from Lucccyo/fix_deps_dune Fix dependancies in `ortac-dune`

Jul 07 14:58 +00:00

Passed in 3m22s

Merge pull request #338 from ocaml-gospel/revert-337-tmp_remove_ortac_monolith Revert "Remove Ortac/Monolith plugin temporarily"

Jul 07 12:32 +00:00

Passed in 4m32s

Merge pull request #337 from Lucccyo/tmp_remove_ortac_monolith Remove Ortac/Monolith plugin temporarily

Jul 03 08:17 +00:00

Failed in 3m28s

Merge pull request #336 from Lucccyo/prepare_release_0.7 Prepare release 0.7

Jul 02 10:31 +00:00

Failed in 35m19s

Merge pull request #335 from Lucccyo/fix_dune_wrapper Fix dune rules for wrapper plugin

Jun 25 13:05 +00:00

Passed in 3m36s

Merge pull request #333 from n-osborne/add-Charlène-as-author Add Charlène Gros as new author

Jun 25 07:43 +00:00

Failed in 2h49m

Merge pull request #332 from Lucccyo/attribute_opt Add a better management of attribute for projection functions

Jun 25 06:43 +00:00

Failed in 52m42s

Merge pull request #331 from Lucccyo/proj_and_value Print projection function as `Ir.Projection` and `Ir.Value`

Jun 23 08:05 +00:00

Failed in 5m14s

Merge pull request #327 from Lucccyo/warn_unprovided Prevent code generation if required model projection is absent

Jun 19 08:46 +00:00

Failed in 3m33s

Merge pull request #326 from n-osborne/fix-next-state-int [QCheck-STM] Fix next-state computation for functions specialised for `int`s

Jun 18 16:16 +00:00

Failed in 16m01s

Merge pull request #324 from Lucccyo/name_conflict Fix naming conflicts between model projections and function arguments

Jun 18 15:37 +00:00

Passed in 20m03s

Merge pull request #322 from Lucccyo/file_gen_info Add header message in generated files with wrapper mode

Jun 12 14:12 +00:00

Failed in 13m57s

Merge pull request #314 from Lucccyo/wrapper_auto_dune Add automatic dune file generation to the wrapper plugin

Jun 11 09:59 +00:00

Passed in 8m41s

Merge pull request #315 from n-osborne/bump-to-dev-version Bump version to dev

Jun 06 15:11 +00:00

Failed in 8m30s

Merge pull request #313 from Lucccyo/fix_model Fix missing model support in preconditions

May 27 07:54 +00:00

Passed in 14m40s

Merge pull request #305 from Lucccyo/add_model Add support for models in the wrapper plugin

May 21 08:49 +00:00

Passed in 14m38s

Merge pull request #307 from n-osborne/qcheck-stm-disable-warning-34 [QCheck-STM] Disable warning 34 in generated code

May 19 11:32 +00:00

Passed in 8m59s

Merge pull request #308 from Lucccyo/reorder_wrapper_gen_tests Reorganise tests into separate files

May 16 09:10 +00:00

Passed in 8m09s

Merge pull request #303 from n-osborne/prepare-0.6.1-release Preparation for 0.6.1 bugfix release

May 12 07:12 +00:00

Passed in 8m43s

Merge pull request #302 from n-osborne/qcheck-stm-named-arguments [QCheck-STM] Fix labelled arguments in runnable scenario

May 07 09:08 +00:00

Failed in 10m15s

Merge pull request #297 from Lucccyo/old_operator Add support for `old` operator in the wrapper plugin

May 06 13:12 +00:00

Passed in 13m30s

Merge pull request #301 from Lucccyo/lwt_dllist_update `lwt_dllist_spec.mli` should meet the implementation of `lwt_dllist`

May 06 09:42 +00:00

Passed in 1h25m

Merge pull request #296 from n-osborne/qcheck-stm-domain [QCheck-STM] Modifies SUTs in place in the store

Apr 18 18:23 +00:00

Failed in 8m10s

Merge pull request #299 from Lucccyo/wrapper-test Add tests to wrapper plugin

Apr 16 12:13 +00:00

Failed in 3m41s

Merge pull request #295 from Lucccyo/violated_errors Fix incorrect error type for violated preconditions and postconditions

Mar 24 16:10 +00:00

Passed in 5m30s

Merge pull request #293 from n-osborne/prepare-release Prepare 0.6.0 release

Mar 18 21:04 +00:00

Passed in 9m33s

Merge pull request #292 from n-osborne/update-deploy-workflow Update deploy-pages version

Mar 04 14:18 +00:00

Passed in 9m19s

Merge pull request #291 from n-osborne/more-flexible-returned-value-description Make search for returned value description more flexible

Mar 04 13:53 +00:00

Failed in 24m34s

Merge pull request #288 from n-osborne/fix-fn-appy-ident-generation Fix generation of the `QCheck.Fn.apply` identifier

Mar 03 14:42 +00:00

Passed in 5m04s

Merge pull request #290 from n-osborne/update-doc-workflow-bis Fix upload-pages-artifact version

Mar 03 14:14 +00:00

Passed in 26m13s

Merge pull request #289 from n-osborne/update-doc-workflow Update gh-pages github workflow

Mar 03 14:05 +00:00

Failed in 5m24s

Merge pull request #287 from n-osborne/partial-functions Improve failure message in case of out of domain failure

Mar 03 12:57 +00:00

Passed in 46m59s

Merge pull request #286 from n-osborne/fix-opam-x-maintenance Fix x-maintenance-intent syntax

Feb 17 23:22 +00:00

Passed in 15m47s

Merge pull request #285 from n-osborne/zero-length-issue Add zero-length bitv issue in README

Jan 13 16:16 +00:00

Merge pull request #284 from n-osborne/release-preparation release preparation

Jan 06 15:45 +00:00

Passed in 9m14s

Merge pull request #283 from n-osborne/x-maintenance-intent Add x-maintenance-intent field in opam files

Jan 06 14:23 +00:00

Failed in 34m16s

Merge pull request #282 from n-osborne/update-ocamlformat.0.27.0 update ocamlformat.0.27.0

Jan 06 09:50 +00:00

Failed in 22m53s

Merge pull request #281 from n-osborne/submodule-cli-option Add `submodule` optional argument to Ortac/QCheck-STM and Ortac/Dune

Jan 06 09:49 +00:00

Merge pull request #280 from n-osborne/module-prefix-cli-option Add `module-prefix` optional argument to Ortac/QCheck-STM and Ortac/Dune

Dec 19 16:03 +00:00

Failed in 8m53s

Merge pull request #277 from jmid/fun-gen-support-cleanup Add function generation support

Dec 16 14:26 +00:00

Passed in 2h13m

Merge pull request #279 from n-osborne/move-tests-to-sequence Replace lists by sequences in Ortac/QCheck-STM tests

Dec 10 13:15 +00:00

Failed in 33m52s

Merge pull request #276 from jmid/rm-left-over-limitation Remove left-over multiple-ts limitation from QCheck-STM README

Dec 03 16:47 +00:00

Failed in 21m18s

Merge pull request #275 from jmid/fix-unkown-kind Fix Unkown_kind

Dec 03 16:45 +00:00

Failed in 1m45s

Merge pull request #271 from nikolaushuber/extend-qcheck-stm-tests Extend tests of the QCheck-STM plugin

Nov 19 18:58 +00:00

Passed in 12m09s

Merge pull request #266 from n-osborne/update-github-action Update github action

Nov 03 23:04 +00:00

Passed in 17m23s

Merge pull request #264 from nikolaushuber/clean-postcond Remove unnecessary stack access from precond

Oct 10 07:52 +00:00

Passed in 8m23s

Merge pull request #265 from n-osborne/fix-version-with-test Add missing upper bounds on ortac packages

Oct 09 15:47 +00:00

Passed in 1m50s

Merge pull request #263 from n-osborne/prepare-0.4.0-release Prepare release of version 0.4.0

Oct 08 11:46 +00:00

Passed in 7m25s

Merge pull request #262 from n-osborne/update-documentation Update Ortac/QCheck-STM documentation

Oct 08 07:49 +00:00

Passed in 8m16s

Merge pull request #261 from n-osborne/add-found-bugs Update Ortac/QCheck-STM Readme with found bugs

Oct 08 07:40 +00:00

Merge pull request #259 from nikolaushuber/fork-prop-env Add support for running tests in separate processes with a timeout

Oct 04 07:39 +00:00

Failed in 17m50s

Merge pull request #250 from n-osborne/refactor-reserr Some refactoring of `Reserr`

Oct 02 09:22 +00:00

Passed in 21m27s

Merge pull request #251 from n-osborne/fix-runnable-scenario Fix display of the runnable scenario for protected values

Oct 02 07:28 +00:00

Passed in 45m01s

Merge pull request #253 from nikolaushuber/returning-sut Returning SUT values

Sep 27 16:46 +00:00

Passed in 39m38s

Merge pull request #249 from nikolaushuber/fix-invariants Fix invariant bug with multiple suts

Sep 05 11:54 +00:00

Passed in 7m47s

Merge pull request #247 from nikolaushuber/multi-sut Add support for multiple sut arguments

Sep 01 14:12 +00:00

Passed in 15m17s

Merge pull request #246 from n-osborne/dependencies-cleanup Clean up some dependencies

Aug 21 14:39 +00:00

Failed in 15m40s

Merge pull request #245 from nikolaushuber/sut-as-type-inst Sut as type argument or inside tuple

Jul 29 13:57 +00:00

Passed in 4m44s

Merge pull request #244 from n-osborne/minimal-monolith-version-bis Update dune-project with monolith minimal version

Jul 17 11:42 +00:00

Passed in 48m38s

Merge pull request #243 from n-osborne/minimal-monolith-version Add minimal version for Monolith

Jul 15 17:33 +00:00

Passed in 49m18s

Merge pull request #241 from n-osborne/prepare-0.3.0-release prepare 0.3.0 release

Jul 04 09:01 +00:00

Failed in 6d05h

Merge pull request #242 from nikolaushuber/mention-dune-plugin Mention dune-rules plugin in qcheck-stm README

Jul 03 15:43 +00:00

Passed in 49m03s

Merge pull request #226 from n-osborne/stm-cleanup Read optional `cleanup` function from configuration module

Jul 01 15:17 +00:00

Passed in 12m13s

Merge pull request #229 from n-osborne/fix-field-access-printing Fix field access translation

Jul 01 14:07 +00:00

Merge pull request #239 from n-osborne/use-ppxlib-longident Use existing functionaly from `Ppxlib.Longident`

Jul 01 13:43 +00:00

Passed in 16m07s

Merge pull request #230 from n-osborne/functional-model Add support for functional models

Jul 01 13:42 +00:00

Merge pull request #218 from n-osborne/revise-dune-plugin Revise Ortac/Dune to minimize yet again boilerplate

Jul 01 12:16 +00:00

Passed in 17m54s

Merge pull request #240 from nikolaushuber/incomplete-comp-warning Remove bug with integers in return values

Jul 01 11:52 +00:00

Passed in 19m36s

Merge pull request #237 from nikolaushuber/tuples Add support for tuples

Jun 26 08:21 +00:00

Passed in 1h30m

Merge pull request #235 from nikolaushuber/test-without-sut Add support for functions without SUT argument

Jun 17 14:03 +00:00

Passed in 1h09m

Merge pull request #234 from nikolaushuber/empty-cmd-error Add empty cmd error

Jun 06 12:42 +00:00

Passed in 29m47s

Merge pull request #214 from n-osborne/module-based-config Move to a module based configuration

Jun 04 11:15 +00:00

Failed in 17h34m

Merge pull request #228 from n-osborne/support-custom-ghost-types Add support for custom ghost type as model

May 29 14:36 +00:00

Passed in 14m02s

Merge pull request #227 from n-osborne/add-doc-for-ocaml_file Add doc for `ocaml_file` Cmdliner arg

May 16 11:32 +00:00

Failed in 1h22m

Merge pull request #225 from n-osborne/update-ocamlformat Update ocamlformat to 0.26.2

May 16 09:42 +00:00

Passed in 16m52s

Merge pull request #223 from n-osborne/fix-lower-bounds Fix lower bounds

May 10 08:50 +00:00

Merge pull request #222 from n-osborne/hotfix Add missing dependency

Apr 15 09:27 +00:00

Passed in 23m45s

Merge pull request #221 from n-osborne/bump-version-0.2.0-bis Propagate dune-project changes to opam files

Apr 15 08:50 +00:00

Passed in 5m33s

Merge pull request #220 from n-osborne/bump-version-to-0.2.0 Bump version number

Apr 15 07:13 +00:00

Passed in 8m48s

Merge pull request #217 from n-osborne/default-term Move to use a default `Cmdliner.term` rather than the `usage` function

Apr 15 06:54 +00:00

Passed in 15m54s

Merge pull request #211 from n-osborne/consistent-ocaml-version Bump all OCaml version to the same number

Apr 12 12:25 +00:00

Passed in 11m24s

Merge pull request #219 from n-osborne/update-gospel Update to gospel.0.3.0

Apr 12 12:04 +00:00

Passed in 1m53s

Merge pull request #215 from n-osborne/dune-build-info Use `dune-build-info` rather than `dune subst`

Apr 09 10:06 +00:00

Passed in 12m45s

Merge pull request #206 from n-osborne/print-exn-result Add support for exceptional behaviour to printing runnable scenario

Mar 27 16:25 +00:00

Passed in 35m00s

Merge pull request #210 from shym/cram-typos Fix a small bug in a cram test and some typos

Mar 18 09:35 +00:00

Passed in 33m10s

Merge pull request #204 from n-osborne/print-runnable-scenario Print runnable scenario in case of test failure

Mar 18 09:09 +00:00

Failed in 16m09s

Merge pull request #202 from n-osborne/failure-message Improve failure message

Mar 14 10:34 +00:00

Passed in 31m50s

Add support for type invariants (#197) * Cleanup a bit Ir_of_gospel.state function * Add some new functions to Builder Mostly add `list_or` and `enot` that will soon be needed, but take the opportunity to move `qualify` and redefine some functions that where worngfully using `evar` on qualified names. * Add invariants in intermediate representation * Translate invariants and check them in postcond This will guarantee preservation of type invariants for `sut` * Check type invariants in `init_state` and add some tests * Update Changelog

Mar 13 15:10 +00:00

Add a comment at BOF warning that it is a generated file (#198)

Feb 29 14:02 +00:00

Merge pull request #190 from n-osborne/ortac-dune ortac-dune plugin

Feb 12 13:42 +00:00

Passed in 1h13m

update to latest gospel (#194) * Add a pin to last version of gospel Representation of type invariants were modified. * Update ortac wrapper to new gospel

Jan 31 11:16 +00:00

Passed in 9m32s

Merge pull request #193 from shym/deploy-gh-3 github pages deployment, take 3

Jan 11 17:54 +00:00

Passed in 38m41s