Merge pull request #15 from Yag000/ci-on-pr

Run the ci on PRs from foreign repos

.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,

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;
     };
   ]
 

bin/uiml_cmdline.ml

@@ -1,4 +1,4 @@
-open ExEnum
+open Exenum
 open Printer
 open UIML.Formulas
 open Sys