diff --git a/.github/workflows/build_docs.yml b/.github/workflows/build_docs.yml index 2af6456..7acf925 100644 --- a/.github/workflows/build_docs.yml +++ b/.github/workflows/build_docs.yml @@ -2,11 +2,16 @@ name: Build doc on: push: + pull_request: jobs: build: name: Build docs runs-on: ubuntu-latest + + # Avoid running twice the action if it's triggered by a push on a PR from a branch on the repo. + if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name != github.event.pull_request.base.repo.full_name + container: image: coqorg/coq:8.19 # This is a workaround a "bug" on the checkout action, diff --git a/bin/benchmark.ml b/bin/benchmark.ml index 61be81e..4b1101b 100644 --- a/bin/benchmark.ml +++ b/bin/benchmark.ml @@ -1,14 +1,7 @@ open UIML.UIML_extraction open UIML.Formulas open Modal_expressions_parser - -let rec weight = function - | Bot -> 1 - | Var _ -> 1 - | And (f1, f2) -> 2 + weight f1 + weight f2 - | Or (f1, f2) -> 3 + weight f1 + weight f2 - | Implies (f1, f2) -> 1 + weight f1 + weight f2 - | Box f -> 1 + weight f +open Printer type 'a timed_result = { value : 'a; time : float } @@ -41,13 +34,13 @@ let bench_one fs = [ { name = "A " ^ fs; - before = time (fun f -> weight (isl_A [ 'p' ] f)) f; - after = time (fun f -> weight (isl_simplified_A [ 'p' ] f)) f; + before = time (fun f -> int_of_nat (weight (isl_A [ 'p' ] f))) f; + after = time (fun f -> int_of_nat (weight (isl_simplified_A [ 'p' ] f))) f; }; { name = "E " ^ fs; - before = time (fun f -> weight (isl_E [ 'p' ] f)) f; - after = time (fun f -> weight (isl_simplified_E [ 'p' ] f)) f; + before = time (fun f -> int_of_nat (weight (isl_E [ 'p' ] f))) f; + after = time (fun f -> int_of_nat (weight (isl_simplified_E [ 'p' ] f))) f; }; ] diff --git a/bin/uiml_cmdline.ml b/bin/uiml_cmdline.ml index c65ab88..3652d87 100644 --- a/bin/uiml_cmdline.ml +++ b/bin/uiml_cmdline.ml @@ -1,4 +1,4 @@ -open ExEnum +open Exenum open Printer open UIML.Formulas open Sys