Split development in multiple packages and projects

epfl-systemf · Aug 4, 2024 · 4a13154 · 4a13154
1 parent d065be9
commit 4a13154
Show file tree

Hide file tree

Showing 27 changed files with 89 additions and 35 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -91,10 +91,6 @@ jobs:
               opam install --confirm-level=unsafe-yes .
               echo "::endgroup::"
 
-              echo "::group::List installed files"
-              tree /home/runner/work/Warblre/Warblre/_opam
-              echo "::endgroup::"
-
               echo "::group::Uninstall Warblre"
               opam remove --confirm-level=unsafe-yes .
               echo "::endgroup::"

diff --git a/README.md b/README.md
@@ -78,17 +78,19 @@ The repository is structured as follows:
 │   ├── cmd_playground
 │   ├── coq_proof
 │   └── ocaml_example
-├── fuzzer
-├── tests
-└── test262
+└── tests
+    ├── tests
+    ├── fuzzer
+    └── test262
 ```
 
 - **[Mechanization](#mechanization)**: Warblre proper, the mechanization in Coq of the ECMASCript semantics of regexes.
 - **[Engines](#engines)**: Extraction directives and extra code to allow a smooth usage of the extracted engine in different programming languages. Most of the code is in `common`; the other directories contain code specific to one particular language.
 - **Examples**: Code snippets which show how to use the mechanization and extracted engines.
-- **Fuzzer**: A differential fuzzer comparing the extracted JavaScript engine with the one from the host JavaScript environment.
-- **Tests**: Unit tests for the OCaml engine.
-- **Test262**: A thin wrapper which allows to test the extracted JavaScript engine against [Test262](https://github.com/tc39/test262), the standard test suite for JavaScript engines; see the related [documentation](doc/Test262.md).
+- **Tests:**
+  - **Tests**: Unit tests for the OCaml engine.
+  - **Fuzzer**: A differential fuzzer comparing the extracted JavaScript engine with the one from the host JavaScript environment.
+  - **Test262**: A thin wrapper which allows to test the extracted JavaScript engine against [Test262](https://github.com/tc39/test262), the standard test suite for JavaScript engines; see the related [documentation](doc/Test262.md).
 
 The follow subsections further detail some of these.
 

diff --git a/dune-project b/dune-project
@@ -8,19 +8,25 @@
 (using melange 0.1)
 (using directory-targets 0.1)
 
+(homepage "https://github.com/epfl-systemf/warblre")
+(authors "Noé De Santo" "Aurèle Barrière" "Clément Pit-Claudel")
+(maintainers "Noé De Santo" "Aurèle Barrière")
+(bug_reports "https://github.com/epfl-systemf/warblre/issues")
+(license BSD-3-Clause)
+
 (package
  (name warblre)
- (homepage "https://github.com/epfl-systemf/warblre")
- (authors "Noé De Santo" "Aurèle Barrière" "Clément Pit-Claudel")
  (synopsis "A mechanization of the specification of ECMAScript regexes")
- (maintainers "Noé De Santo" "Aurèle Barrière")
- (bug_reports "https://github.com/epfl-systemf/warblre/issues")
- (license BSD-3-Clause)
  (depends
-  (ocaml (= 4.14.2))
-  (coq (>= 8.18.0))
+  (ocaml (= 4.14.2))))
+
+(package
+ (name warblre-engines)
+ (synopsis "Regex engines extracted from Warblre")
+ (depends
+  (warblre (= :version))
   (integers (>= 0.7.0))
   (uucp (>= 15.0.0))
   (zarith (>= 1.13))
   (melange (= 3.0.0-414))
-  (ppx_expect (>= v0.16.0))))
+  (ppx_expect (>= v0.16.0))))
diff --git a/engines/js/dune b/engines/js/dune
@@ -15,7 +15,7 @@
 ; Make a library out of it
 (library
  (name warblre_js)
- (public_name warblre.js)
+ (public_name warblre-engines.js)
  (libraries melange.belt)
  (melange.runtime_deps (file ./regexpp-map.mjs))
  (modes melange)

diff --git a/engines/ocaml/dune b/engines/ocaml/dune
@@ -15,7 +15,7 @@
 ; Make a library out of it
 (library
  (name warblre)
- (public_name warblre.ocaml)
+ (public_name warblre-engines.ocaml)
  (libraries uucp integers zarith))
 
 (env

diff --git a/examples/browser_playground/dune b/examples/browser_playground/dune
@@ -2,7 +2,7 @@
  (alias browser-playground-js)
  (target app)
  (module_systems (es6 mjs))
- (libraries melange.dom warblre_js)
+ (libraries melange.dom warblre-engines.js)
  (preprocess (pps melange.ppx)))
 
 ; Webpack it into a single, browser-compatible, js file

diff --git a/examples/cmd_playground/dune b/examples/cmd_playground/dune
@@ -2,7 +2,7 @@
  (alias node-playground-js)
  (target app)
  (module_systems (es6 mjs))
- (libraries melange.dom warblre_js)
+ (libraries melange.dom warblre-engines.js)
  (preprocess (pps melange.ppx)))
 
 ; Webpack it into a single, node-compatible, js file

diff --git a/examples/dune-project b/examples/dune-project
@@ -0,0 +1,12 @@
+(lang dune 3.14)
+; This package is defined in a sub dune-project to prevent the installation of example executables
+
+(generate_opam_files false)
+
+(using melange 0.1)
+(using directory-targets 0.1)
+
+(package
+ (name warblre-examples)
+ (depends
+  warblre-engines))
diff --git a/examples/ocaml_example/dune b/examples/ocaml_example/dune
@@ -1,4 +1,3 @@
 (executable
- (public_name example)
  (name main)
- (libraries warblre))
+ (libraries warblre-engines.ocaml))
diff --git a/tests/dune-project b/tests/dune-project
@@ -0,0 +1,12 @@
+(lang dune 3.14)
+; This package is defined in a sub dune-project to prevent the installation of test executables
+
+(generate_opam_files false)
+
+(using melange 0.1)
+(using directory-targets 0.1)
+
+(package
+ (name warblre-tests)
+ (depends
+  warblre-engines))
diff --git a/fuzzer/Fuzzer.ml → tests/fuzzer/Fuzzer.ml b/fuzzer/Fuzzer.ml → tests/fuzzer/Fuzzer.ml
diff --git a/fuzzer/dune → tests/fuzzer/dune b/fuzzer/dune → tests/fuzzer/dune
@@ -2,15 +2,15 @@
  (alias fuzzer-js)
  (target app)
  (module_systems (es6 mjs))
- (libraries warblre_js)
+ (libraries warblre-engines.js)
  (preprocess (pps melange.ppx)))
 
 ; Webpack it into a single, browser-compatible, js file
 (rule
  (target warblre-node-fuzzer.js)
  (deps
   (alias_rec fuzzer-js)
-  (:entrypoint (file app/fuzzer/Fuzzer.mjs))
+  (:entrypoint (file app/tests/fuzzer/Fuzzer.mjs))
   (:config (file webpack.config.js)))
  (action (no-infer (progn
   (run npx webpack ./%{entrypoint} --config %{config} --no-stats)

diff --git a/fuzzer/webpack.config.js → tests/fuzzer/webpack.config.js b/fuzzer/webpack.config.js → tests/fuzzer/webpack.config.js
diff --git a/test262/Redirect.ml → tests/test262/Redirect.ml b/test262/Redirect.ml → tests/test262/Redirect.ml
diff --git a/test262/dune → tests/test262/dune b/test262/dune → tests/test262/dune
@@ -2,15 +2,15 @@
  (alias test262-js)
  (target app)
  (module_systems (es6 mjs))
- (libraries warblre_js)
+ (libraries warblre-engines.js)
  (preprocess (pps melange.ppx)))
 
 ; Webpack it into a single, browser-compatible, js file
 (rule
  (targets warblre-node-redirect.js warblre-browser-redirect.js)
  (deps
   (alias_rec test262-js)
-  (:entrypoint (file app/test262/Redirect.mjs))
+  (:entrypoint (file app/tests/test262/Redirect.mjs))
   (:config (file webpack.config.js)))
  (action (no-infer (progn
   (run npx webpack ./%{entrypoint} --config %{config} --no-stats)

diff --git a/test262/webpack.config.js → tests/test262/webpack.config.js b/test262/webpack.config.js → tests/test262/webpack.config.js
diff --git a/tests/Backrefs.ml → tests/tests/Backrefs.ml b/tests/Backrefs.ml → tests/tests/Backrefs.ml
diff --git a/tests/BoundaryAssertions.ml → tests/tests/BoundaryAssertions.ml b/tests/BoundaryAssertions.ml → tests/tests/BoundaryAssertions.ml
diff --git a/tests/Counterexample.ml → tests/tests/Counterexample.ml b/tests/Counterexample.ml → tests/tests/Counterexample.ml
diff --git a/tests/Exec.ml → tests/tests/Exec.ml b/tests/Exec.ml → tests/tests/Exec.ml
diff --git a/tests/Lookarounds.ml → tests/tests/Lookarounds.ml b/tests/Lookarounds.ml → tests/tests/Lookarounds.ml
diff --git a/tests/Printer.ml → tests/tests/Printer.ml b/tests/Printer.ml → tests/tests/Printer.ml
diff --git a/tests/Tests.ml → tests/tests/Tests.ml b/tests/Tests.ml → tests/tests/Tests.ml
diff --git a/tests/UnicodeAlphabetic.ml → tests/tests/UnicodeAlphabetic.ml b/tests/UnicodeAlphabetic.ml → tests/tests/UnicodeAlphabetic.ml
diff --git a/tests/dune → tests/tests/dune b/tests/dune → tests/tests/dune
@@ -1,6 +1,6 @@
 (library
  (name tests)
- (libraries warblre)
+ (libraries warblre-engines.ocaml)
  (inline_tests)
  (preprocess
   (pps ppx_expect)))
diff --git a/warblre-engines.opam b/warblre-engines.opam
@@ -0,0 +1,32 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Regex engines extracted from Warblre"
+maintainer: ["Noé De Santo" "Aurèle Barrière"]
+authors: ["Noé De Santo" "Aurèle Barrière" "Clément Pit-Claudel"]
+license: "BSD-3-Clause"
+homepage: "https://github.com/epfl-systemf/warblre"
+bug-reports: "https://github.com/epfl-systemf/warblre/issues"
+depends: [
+  "dune" {>= "3.14"}
+  "warblre" {= version}
+  "integers" {>= "0.7.0"}
+  "uucp" {>= "15.0.0"}
+  "zarith" {>= "1.13"}
+  "melange" {= "3.0.0-414"}
+  "ppx_expect" {>= "v0.16.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
diff --git a/warblre.opam b/warblre.opam
@@ -3,17 +3,12 @@ opam-version: "2.0"
 synopsis: "A mechanization of the specification of ECMAScript regexes"
 maintainer: ["Noé De Santo" "Aurèle Barrière"]
 authors: ["Noé De Santo" "Aurèle Barrière" "Clément Pit-Claudel"]
+license: "BSD-3-Clause"
 homepage: "https://github.com/epfl-systemf/warblre"
 bug-reports: "https://github.com/epfl-systemf/warblre/issues"
 depends: [
   "dune" {>= "3.14"}
   "ocaml" {= "4.14.2"}
-  "coq" {>= "8.18.0"}
-  "integers" {>= "0.7.0"}
-  "uucp" {>= "15.0.0"}
-  "zarith" {>= "1.13"}
-  "melange" {= "3.0.0-414"}
-  "ppx_expect" {>= "v0.16.0"}
   "odoc" {with-doc}
 ]
 build: [