diff --git a/.github/pip-requirements.txt b/.github/pip-requirements.txt index 153043b..c26e924 100644 --- a/.github/pip-requirements.txt +++ b/.github/pip-requirements.txt @@ -1,4 +1,4 @@ -alectryon == 1.4.0 +alectryon @ git+https://github.com/cpitclaudel/alectryon@a02a99c75c4166efc8812a600e8cbf4588424c0f git+https://github.com/epfl-systemf/SpecMerger -requests == 2.32.3 +requests == 2.32.4 beautifulsoup4 == 4.12.3 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4cf0e04..efd8bbe 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -14,15 +14,15 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - coq: [ "8.18.0", "8.19.2" ] - node: [ "21.7.2", "22.4.1" ] + rocq: [ "9.0.0", "9.1.0" ] + node: [ "24.13.0" ] fail-fast: false steps: - name: Checkout repository - uses: actions/checkout@v4 + uses: actions/checkout@v6 - name: Install Node.js - uses: actions/setup-node@v4 + uses: actions/setup-node@v6 with: node-version: ${{ matrix.node }} cache: 'npm' @@ -51,9 +51,9 @@ jobs: uses: actions/cache@v4 with: path: /home/runner/work/Warblre/Warblre/_opam - key: opam-packages-cache-${{runner.os}}-coq${{matrix.coq}}-${{ hashFiles('**/*.opam') }} + key: opam-packages-cache-${{runner.os}}-rocq${{matrix.rocq}}-${{ hashFiles('**/*.opam') }} restore-keys: | - opam-packages-cache-${{runner.os}}-coq${{matrix.coq}} + opam-packages-cache-${{runner.os}}-rocq${{matrix.rocq}} opam-packages-cache-${{runner.os}} - name: Install opam dependencies run: | @@ -62,10 +62,8 @@ jobs: echo "::endgroup::" echo "::group::Install opam packages" - opam pin add -n -k version coq ${{ matrix.coq }} - # coq-serapi's dependencies are installed now to ensure - opam install --confirm-level=unsafe-yes --deps-only . coq-serapi - opam install --confirm-level=unsafe-yes coq-serapi + opam pin add -n -k version coq ${{ matrix.rocq }} + opam install --confirm-level=unsafe-yes --deps-only . echo "::endgroup::" echo "::group::Print opam config (post-install)" @@ -80,10 +78,10 @@ jobs: run: | opam exec -- dune test --force --display=verbose - - name: Check compiled libraries (coqchk) + - name: Check compiled libraries (rocqchk) run: | ALL_VOS=$(find _build/default/mechanization/ -name '*.vo'); - opam exec -- coqchk -silent --output-context -Q _build/default/mechanization Warblre $ALL_VOS + opam exec -- rocqchk -silent --output-context -Q _build/default/mechanization Warblre $ALL_VOS - name: Test install of Warblre run: | diff --git a/.gitignore b/.gitignore index 608e60e..fe25899 100644 --- a/.gitignore +++ b/.gitignore @@ -1,10 +1,16 @@ -# Coq(ide) generated files +# Rocq/CoqIDE generated files .lia.cache \#*\# +# This file gets generated by dune, and contains install-dependent paths +_RocqProject + # Dune's build directory _build/ +# Opam's directory +_opam/ + # VsCode's configuration .vscode/ @@ -16,4 +22,4 @@ _build/ node_modules # python -*/__pycache__ \ No newline at end of file +*/__pycache__ diff --git a/.nix/dune.nix b/.nix/dune.nix new file mode 100644 index 0000000..86d3373 --- /dev/null +++ b/.nix/dune.nix @@ -0,0 +1,57 @@ +# Based on +# https://github.com/NixOS/nixpkgs/blob/2375cc015c9c2d5dfaff876d063cd9218ae89a84/pkgs/development/tools/ocaml/dune/3.nix + +{ + lib, + stdenv, + fetchurl, + ocaml, + findlib, + ocaml-lsp, + dune-release, + fetchFromGitHub, +}: + +stdenv.mkDerivation rec { + pname = "dune"; + version = "3.21.0"; + + src = fetchFromGitHub { + owner = "ocaml"; + repo = "dune"; + rev = "6e9d965bb5bbadfe9cbf89314cb6f8ecaa845bd9"; + hash = "sha256-YOey/GwrJVrQwEgoV8taDF6t6LgCJtrtmPQPvAtA7EQ="; + }; + + nativeBuildInputs = [ + ocaml + findlib + ]; + + strictDeps = true; + + buildFlags = [ "release" ]; + + dontAddPrefix = true; + dontAddStaticConfigureFlags = true; + configurePlatforms = [ ]; + + installFlags = [ + "PREFIX=${placeholder "out"}" + "LIBDIR=$(OCAMLFIND_DESTDIR)" + ]; + + passthru.tests = { + inherit ocaml-lsp dune-release; + }; + + meta = { + homepage = "https://dune.build/"; + description = "Composable build system"; + mainProgram = "dune"; + changelog = "https://github.com/ocaml/dune/raw/${version}/CHANGES.md"; + maintainers = [ lib.maintainers.vbgl ]; + license = lib.licenses.mit; + inherit (ocaml.meta) platforms; + }; +} \ No newline at end of file diff --git a/.nix/vsrocq-language-server.nix b/.nix/vsrocq-language-server.nix new file mode 100644 index 0000000..62dc56b --- /dev/null +++ b/.nix/vsrocq-language-server.nix @@ -0,0 +1,65 @@ +# Based on +# https://github.com/NixOS/nixpkgs/blob/nixos-25.11/pkgs/development/rocq-modules/vsrocq-language-server/default.nix + +{ + metaFetch, + coq_9_1, + rocq-core_9_1, + lib, + glib, + adwaita-icon-theme, + wrapGAppsHook3, + fetchFromGitHub, +}: + +let + ocamlPackages = rocq-core_9_1.ocamlPackages; + + repo = fetchFromGitHub { + owner = "rocq-prover"; + repo = "vsrocq"; + rev = "v2.3.4"; + hash = "sha256-v1hQjE8U1o2VYOlUjH0seIsNG+NrMNZ8ixt4bQNyGvI="; + }; +in +ocamlPackages.buildDunePackage { + pname = "vsrocq-language-server"; + version = "2.3.4"; + src = "${repo}/language-server"; + nativeBuildInputs = [ coq_9_1 ]; + buildInputs = [ + coq_9_1 + glib + adwaita-icon-theme + wrapGAppsHook3 + ] + ++ (with ocamlPackages; [ + findlib + lablgtk3-sourceview3 + zarith + ppx_inline_test + ppx_assert + ppx_sexp_conv + ppx_deriving + ppx_import + sexplib + (ppx_yojson_conv.override { + ppx_yojson_conv_lib = ppx_yojson_conv_lib.override { yojson = yojson_2; }; + }) + lsp + sel + ppx_optcomp + ]); + preBuild = '' + make dune-files + ''; + + meta = + with lib; + { + description = "Language server for the vsrocq vscode/codium extension"; + homepage = "https://github.com/rocq-prover/vsrocq"; + maintainers = with maintainers; [ cohencyril ]; + license = licenses.mit; + }; +} \ No newline at end of file diff --git a/README.md b/README.md index 971397d..5c06232 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ -# Warblre: A Coq mechanization of ECMAScript regexes +# Warblre: A Rocq mechanization of ECMAScript regexes -This repository contains *Warblre*, a Coq mechanization of ECMAScript regexes. +This repository contains *Warblre*, a Rocq mechanization of ECMAScript regexes. [ECMAScript](https://ecma-international.org/publications-and-standards/standards/ecma-262/) is the specification followed by JavaScript implementations, and a mechanization of its regex semantics makes it possible to reason formally about these regexes from a proof assistant. The mechanization has the following properties: @@ -26,23 +26,17 @@ The mechanization has the following properties: ```shell opam install . --deps-only ``` - This will allow you to step through the Coq code, extract the OCaml code and compile it. + This will allow you to step through the Rocq code, extract the OCaml code and compile it. 2. **[Optional]** In order to pack and and run the JavaScript code, you will need to install [Node.js](https://nodejs.org/en), e.g. using [nvm](https://github.com/nvm-sh/nvm). ```shell - nvm install 21.7.2 + nvm install 24.13.0 ``` as well as some JavaScript dependencies: ```shell npm install # Install packages used by our JavaScript code npm install -g webpack-cli # Install webpack-cli, which is used to pack the code in monolithic JavaScript files ``` -3. **[Optional]** - [Alectryon](https://github.com/cpitclaudel/alectryon) is used to produced literate examples. - You will also need [serapi](https://github.com/ejgallego/coq-serapi). - ``` - opam install coq-serapi - ``` Alternatively, a [nix](https://nixos.org/) flake installing all the dependencies is provided: ``` @@ -55,7 +49,7 @@ npm install - `dune exec example` will run an example of matching a string with a regex ([source](examples/ocaml_example/Main.ml)). - **[Requires JavaScript dependencies]** `dune exec fuzzer` will build and run the fuzzer to compare the extracted engine against Irregexp (Node.js's regex engine). -- `dune build examples/coq_proof` will build everything so that you can step through [examples/coq-proof/Example.v](examples/coq_proof/Example.v), which demonstrates how Warblre can be used to reason about JavaScript regexes. Alternatively, if you installed Alectryon, you can open the generated [webpage](_build/default/examples/coq_proof/Example.html) in your web browser. +- `dune build examples/rocq_proof` will build everything so that you can step through [examples/rocq-proof/Example.v](examples/rocq_proof/Example.v), which demonstrates how Warblre can be used to reason about JavaScript regexes. ## Structure of the repository @@ -76,7 +70,7 @@ The repository is structured as follows: ├── examples │ ├── browser_playground │ ├── cmd_playground -│ ├── coq_proof +│ ├── rocq_proof │ └── ocaml_example └── tests ├── tests @@ -84,7 +78,7 @@ The repository is structured as follows: └── test262 ``` -- **[Mechanization](#mechanization)**: Warblre proper, the mechanization in Coq of the ECMASCript semantics of regexes. +- **[Mechanization](#mechanization)**: Warblre proper, the mechanization in Rocq 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. - **Tests:** @@ -96,7 +90,7 @@ The follow subsections further detail some of these. ## Mechanization -The `mechanization` directory contains the Coq code mechanizing the subset of the ECMAScript specification which describes regexes and their semantics. +The `mechanization` directory contains the Rocq code mechanizing the subset of the ECMAScript specification which describes regexes and their semantics. It is based on the 14th edition from June 2023, available [here](https://262.ecma-international.org/14.0/). Regexes are described in chapter [22.2](https://tc39.es/ecma262/2023/multipage/text-processing.html#sec-regexp-regular-expression-objects). @@ -115,7 +109,7 @@ The mechanization depends on external types and parameters (for instance for uni This is encoded with a functor, whose parameter is described in `mechanization/spec/API.v`. Files are organized as follows: -- **spec**: the mechanization in itself, translating the paper specification into Coq. +- **spec**: the mechanization in itself, translating the paper specification into Rocq. - **props**: proofs about the specification. The main proofs are - *Compilation failure-free*: if a regex is early-errors-free, then its compilation into a matcher does not raise an error. - *Matching failure-free*: if a matcher is provided with valid inputs, then the matching process does not raise an error. diff --git a/doc/Differences.md b/doc/Differences.md index 7eb2c7b..66a21d7 100644 --- a/doc/Differences.md +++ b/doc/Differences.md @@ -110,15 +110,15 @@ The specification contains a few assertions which ensure that numbers can be saf > >> Assert: n < 2^32 - 1. -These checks are currently not mechanized, as unbound integers are used in Coq, OCaml and JavaScript. +These checks are currently not mechanized, as unbound integers are used in Rocq, OCaml and JavaScript. ## Non-structurally recursive functions Some functions in the specification, `RepeatMatcher` being the the most infamous one, are generally recursive. -Such definitions would be rejected by Coq, as it cannot syntactically ensure their termination. +Such definitions would be rejected by Rocq, as it cannot syntactically ensure their termination. We modified such definitions into fuel-based functions. -This transformation allows Coq to ensure their termination, +This transformation allows Rocq to ensure their termination, since the function is then structurally recursive on the fuel (which is represented using a `nat`). Intuitively, the equivalence of the two functions (before and after transformation) relies on being able to compute a sufficient amount of fuel **prior** to the first call, and on the fact that such a fuel amount exists to begin with. @@ -200,11 +200,14 @@ Some of these other functions were mechanized (`CodePointAt`, `AdvanceStringInde The axiomatization of functions left abstract is *minimal*, in the sense that only axioms which are necessary to ensure the safety and termination of the specification: these functions should most likely satisfy other properties to be considered correct. > For instance, `canonicalize` has no applicable axiom, which would allow for characters such that -> ```Coq +> +> ```rocq > canonicalize c1 = c2 /\ canonicalize c2 = c1 > ``` +> > which would yield some surprising behaviors. In fact, `canonicalize` should most likely be idempotent: -> ```Coq +> +> ```rocq > forall c, canonicalize c = canonicalize (canonicalize c) > ``` diff --git a/doc/Implementation.md b/doc/Implementation.md index 15ee288..aa20d60 100644 --- a/doc/Implementation.md +++ b/doc/Implementation.md @@ -3,45 +3,46 @@ Some design choices had to be done during the mechanization. We document here some of them, in hope this will make them easier to understand. -## From Coq to executable engines +## From Rocq to executable engines ### The clean picture -The Coq mechanization can be used to generate executable engines in both OCaml and JavaScript. -The OCaml code is obtained by using Coq's [extraction](https://coq.inria.fr/doc/v8.18/refman/addendum/extraction.html) feature. +The Rocq mechanization can be used to generate executable engines in both OCaml and JavaScript. +The OCaml code is obtained by using Rocq's [extraction](https://rocq-prover.org/doc/v8.18/refman/addendum/extraction.html) feature. OCaml code can then be compiled to JavaScript using the [Melange](https://github.com/melange-re/melange) compiler. -As will be discussed in the [API](#api) section, the Coq mechanization leaves some functions and datatypes abstract. +As will be discussed in the [API](#api) section, the Rocq mechanization leaves some functions and datatypes abstract. These missing pieces are instantiated in each language, using libraries native to that specific language. Note that the engine is instantiated **twice** in each language: once to implement a "regular" engine (without unicode flags), and once to implement a "unicode" engine (with the `u` flag). More precisely: + - **OCaml; non-`u`:** - Characters are represented using `Int16.t` (from the [integers](https://github.com/yallop/ocaml-integers) library). - The [uucp](https://github.com/dbuenzli/uucp) library is used to capitalize characters. + Characters are represented using `Int16.t` (from the [integers](https://github.com/yallop/ocaml-integers) library). + The [uucp](https://github.com/dbuenzli/uucp) library is used to capitalize characters. - **OCaml; `u`:** - Characters are represented using `int`. - Note that `UChar` are not used to allow for surrogate characters, as is allowed in JavaScript strings. - The full case folding function provided by [uucp](https://github.com/dbuenzli/uucp) is used to implement simple case folding. + Characters are represented using `int`. + Note that `UChar` are not used to allow for surrogate characters, as is allowed in JavaScript strings. + The full case folding function provided by [uucp](https://github.com/dbuenzli/uucp) is used to implement simple case folding. - **JavaScript; non-`u`:** - Characters are represented using strings (which is standard in JavaScript). - [`String.toUpperCase`](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/toUpperCase) is used. + Characters are represented using strings (which is standard in JavaScript). + [`String.toUpperCase`](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/toUpperCase) is used. - **JavaScript; `u`:** - Characters are represented using strings (which is standard in JavaScript). - Case folding is implemented using an auto-generated associative map (`engines/js/SimpleFold.ml`). + Characters are represented using strings (which is standard in JavaScript). + Case folding is implemented using an auto-generated associative map (`engines/js/SimpleFold.ml`). ![Extraction/compilation pipeline](../etc/archi.svg) ### The detail: extraction is done twice The previous presentation omits the fact that the OCaml code compiled to JavaScript is not exactly the same as the one used for native compilation. -More precisely, the two are generated from the same Coq code, using the same extraction directives, but the extracted code refers to some `BigInt` type, +More precisely, the two are generated from the same Rocq code, using the same extraction directives, but the extracted code refers to some `BigInt` type, which is implemented differently depending on the end target. For "pure" OCaml, `BigInt` is implemented using [Zarith](https://github.com/ocaml/Zarith). For JavaScript, it is implemented on top of JavaScript's [`BigInt`](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/BigInt). -`BigInt` must be used to ensure that the semantics of Coq's `nat`/`N`/`Z` are preserved after extraction. +`BigInt` must be used to ensure that the semantics of Rocq's `nat`/`N`/`Z` are preserved after extraction. In particular, not extracting to `BigInt` ended up causing incorrect behaviors when using a quantifier whose bounds are close to the maximal integer (as in this [test](https://github.com/tc39/test262/blob/main/test/built-ins/RegExp/quantifier-integer-limit.js) from Test262), in which case the fuel computation might overflow. Additionally, note that Melange's integers are limited to 32 bits (kind of: integers can be bigger, but will be truncated to 32 bits when performing arithmetic; see their [documentation](https://melange.re/v4.0.0/communicate-with-javascript.html#integers)), which means that `BigInt` are needed for arithmetic even if the number never go above `Number.MAX_SAFE_INTEGER`. @@ -49,7 +50,7 @@ Since Melange/dune don't provide a way to provide JavaScript specific implementa ## API -### Coq API: implicit parameter +### Rocq API: implicit parameter See `spec/Parameters.v`. @@ -58,7 +59,8 @@ As described [here](Differences.md#abstraction-layer), some details (character t This abstraction is achieved by parametrizing all functions with a typeclass which contains these abstracted types&operations. This can be achieved by putting all functions manipulating objects from the specification or lemmas reasoning about it in a section defining the parameters of the specification as context parameters. -```Coq + +```rocq Section AboutTheSpec. (* This contains all the parameters of the specification. *) Context `{specParameters: Parameters}. @@ -82,23 +84,27 @@ About canon_square. See `spec/API.v`. One drawback with the aforementioned abstraction mechanism is that types left abstract (such as `Character`), as well as types defined in term of these types (such as `Regex`), are dependent (as in "dependent types") on the `Parameters` argument. -This is fine while working from within Coq, but becomes a problem at extraction. +This is fine while working from within Rocq, but becomes a problem at extraction. Since OCaml doesn't support dependent types, these types are replaced by `Obj.t`, which means that any kind of type-safety is lost. This would force the clients of the OCaml API to rely heavily on `Obj.magic`, which would make the API unsafe and error-prone. This issue is solved in two parts: + 1. The parameters & user facing APIs are repackaged using modules, which solves the issue for abstract types; 2. Other datatypes which are defined using these abstract types are made parametric on the types directly, rather than on `Parameters`. > For instance, instead of defining `Regex` as - > ```Coq + > + > ```rocq > Inductive Regex `{specParameters: Parameters} := > | Char (chr: specParameters.(Character)) (* <- dependent on specParameters *) > | ... > ``` + > > it is defined as - > ```Coq + > + > ```rocq > Inductive Regex {Character: Type} := > | Char (chr: Character) (* <- parametric polymorphism *) > | ... @@ -112,19 +118,24 @@ parameter inference will have to pick that instance, which in turn force the typ > Continuing the previous example: > a marker typeclass for `Character`s is defined -> ```Coq +> +> ```rocq > Class CharacterMarker (T: Type): Prop := mk_character_marker {}. > ``` +> > and `Parameters` provides an instance +> > ``` > Class Parameters := { > Character: Type; > character_marker:: CharacterMarker Character; > ... > }. -> +> ``` +> > And `Regex` gets an extra implicit marker argument -> ```Coq +> +> ```rocq > Inductive Regex {Character: Type} `{CharacterMarker} := > | Char (chr: Character) > | ... @@ -140,19 +151,21 @@ Currently, Unicode support is mostly hand-written, especially on the JavaScript A better solution would be to rely on specialized libraries, e.g. [ICU4X](https://github.com/unicode-org/icu4x). Advantages include: + - Reduces the amount of **unverified** code on our end; - Maintained by the Unicode Consortium, which warrants a certain amount of confidence in the implementation's correctness; - Provides specialized data structures tailored for unicode (e.g. unicode sets), which might improve the extracted engine's performance; - Sketch a clear path toward engines supporting all unicode properties. This was not done for two reasons: + - ICU4X does not offer OCaml support. [ICU4C](https://github.com/unicode-org/icu) could be used instead; - JavaScript support is offered through a WebAssembly library, which should be inlined into our standalone JavaScript files. -### Modules in +### Modules in -The Coq's API could be changed to rely on modules rather than typeclasses. -This doesn't seem to be the preferred way to do such things in Coq, +The Rocq's API could be changed to rely on modules rather than typeclasses. +This doesn't seem to be the preferred way to do such things in Rocq, but this could dramatically reduce the amount of boilerplate needed to provide two different APIs. ### Abstracting (character) sequences diff --git a/dune-project b/dune-project index 1e793ec..d470e1c 100644 --- a/dune-project +++ b/dune-project @@ -1,10 +1,10 @@ -(lang dune 3.14) +(lang dune 3.21) (name warblre) (generate_opam_files true) -(using coq 0.8) +(using rocq 0.11) (using melange 0.1) (using directory-targets 0.1) @@ -19,7 +19,7 @@ (synopsis "A mechanization of the specification of ECMAScript regexes") (depends (ocaml (= 4.14.2)) - (coq (and (>= "8.18.0") (<= "8.19.2"))))) + (rocq-prover (>= 9.0.0)))) (package (name warblre-engines) diff --git a/engines/common/Extraction.v b/engines/common/Extraction.v index 6b6b69f..b1b8f1c 100644 --- a/engines/common/Extraction.v +++ b/engines/common/Extraction.v @@ -1,4 +1,4 @@ -(** Extract from Coq to OCaml for Melange. +(** Extract from Rocq to OCaml for Melange. We will use these extraction directives twice: - Once for "regular" OCaml; @@ -9,13 +9,14 @@ *) From Warblre Require Import Result Base API. -From Coq Require Import ZArith. +From Stdlib Require Import ZArith. -From Coq Require Extraction. +From Stdlib Require Extraction. Extraction Language OCaml. +Set Extraction Output Directory ".". -From Coq Require extraction.ExtrOcamlBasic. -From Coq Require extraction.ExtrOcamlString. +From Stdlib Require extraction.ExtrOcamlBasic. +From Stdlib Require extraction.ExtrOcamlString. (** nat *) Extract Inductive nat => "BigInt.t" [ "BigInt.zero" "BigInt.Nat.succ" ] @@ -39,24 +40,40 @@ Extract Constant Nat.compare => "(fun n m -> if BigInt.equal n m then Eq else (if BigInt.lt n m then Lt else Gt))". (** positive *) +(* Due to the split of the library into Corelib.BindNums.PosDef and + Stdlib.PArith.BindPos, we duplicate all extractions directives to prevent + any unexpcted behaviors where a call unexpectedly end up being in a library + rather than the other. +*) Extract Inductive positive => "BigInt.t" [ "(fun p-> BigInt.add BigInt.one (BigInt.shift_left p 1))" "(fun p-> BigInt.shift_left p 1)" "BigInt.one" ] "Interop.erased". -Extract Inlined Constant Pos.succ => "BigInt.Nat.succ". -Extract Inlined Constant Pos.add => "BigInt.add". -Extract Inlined Constant Pos.eqb => "BigInt.equal". -Extract Constant Pos.compare => - "(fun n m -> if BigInt.equal n m then Eq else (if BigInt.lt n m then Lt else Gt))". -Extract Inlined Constant Pos.to_nat => "(fun x -> x)". +Extract Constant Corelib.BinNums.PosDef.Pos.succ => "BigInt.Nat.succ". +Extract Constant Stdlib.PArith.BinPos.Pos.succ => "BigInt.Nat.succ". +Extract Inlined Constant Corelib.BinNums.PosDef.Pos.add => "BigInt.add". +Extract Inlined Constant Stdlib.PArith.BinPos.Pos.add => "BigInt.add". +Extract Inlined Constant Corelib.BinNums.PosDef.Pos.eqb => "BigInt.equal". +Extract Inlined Constant Stdlib.PArith.BinPos.Pos.add => "BigInt.add". +Extract Constant Corelib.BinNums.PosDef.Pos.compare => + "(fun n m -> if BigInt.equal n m then Eq else (if BigInt.lt n m then Lt else Gt))". +Extract Constant Stdlib.PArith.BinPos.Pos.compare => + "(fun n m -> if BigInt.equal n m then Eq else (if BigInt.lt n m then Lt else Gt))". +Extract Inlined Constant Corelib.BinNums.PosDef.Pos.to_nat => "(fun x -> x)". +Extract Inlined Constant Stdlib.PArith.BinPos.Pos.to_nat => "(fun x -> x)". Extract Constant eqdec_positive => "BigInt.equal". -Extract Constant Pos.add_carry => "Interop.erased". -Extract Constant Pos.pred_double => "Interop.erased". -Extract Constant Pos.compare_cont => "Interop.erased". -Extract Constant Pos.iter_op => "Interop.erased". -Extract Constant Pos.of_succ_nat => "Interop.erased". +Extract Constant Corelib.BinNums.PosDef.Pos.add_carry => "Interop.erased". +Extract Constant Stdlib.PArith.BinPos.Pos.add_carry => "Interop.erased". +Extract Constant Corelib.BinNums.PosDef.Pos.pred_double => "Interop.erased". +Extract Constant Stdlib.PArith.BinPos.Pos.pred_double => "Interop.erased". +Extract Constant Corelib.BinNums.PosDef.Pos.compare_cont => "Interop.erased". +Extract Constant Stdlib.PArith.BinPos.Pos.compare_cont => "Interop.erased". +Extract Constant Corelib.BinNums.PosDef.Pos.iter_op => "Interop.erased". +Extract Constant Stdlib.PArith.BinPos.Pos.iter_op => "Interop.erased". +Extract Constant Corelib.BinNums.PosDef.Pos.of_succ_nat => "Interop.erased". +Extract Constant Stdlib.PArith.BinPos.Pos.of_succ_nat => "Interop.erased". (** Z *) Extract Inductive Z => @@ -89,4 +106,4 @@ Extract Inductive Result.Result => [ "Interop.success" "Interop.error" ] "(fun fS _ v -> fS v )". -Extraction "Extracted.ml" API. \ No newline at end of file +Extraction "Extracted.ml" API. diff --git a/engines/js/dune b/engines/js/dune index b6bff71..4622525 100644 --- a/engines/js/dune +++ b/engines/js/dune @@ -7,10 +7,10 @@ (files ../common/Extraction.v)) ; Extract with different directives -(coq.extraction +(rocq.extraction (prelude Extraction) (extracted_modules Extracted) - (theories Warblre Ltac2)) + (theories Warblre Ltac2 Stdlib)) ; Make a library out of it (library @@ -24,4 +24,4 @@ (env (dev (flags - (:standard -w -27 -w -39 -w -67)))) + (:standard -w -20 -w -27 -w -39 -w -67)))) diff --git a/engines/ocaml/dune b/engines/ocaml/dune index 46b3186..46660fe 100644 --- a/engines/ocaml/dune +++ b/engines/ocaml/dune @@ -7,10 +7,10 @@ (files ../common/Extraction.v)) ; Extract with different directives -(coq.extraction +(rocq.extraction (prelude Extraction) (extracted_modules Extracted) - (theories Warblre Ltac2)) + (theories Warblre Ltac2 Stdlib)) ; Make a library out of it (library @@ -21,4 +21,4 @@ (env (dev (flags - (:standard -w -27 -w -39 -w -67)))) + (:standard -w -20 -w -27 -w -39 -w -67)))) diff --git a/etc/archi.svg b/etc/archi.svg index e7026a7..23bf7b7 100644 --- a/etc/archi.svg +++ b/etc/archi.svg @@ -822,7 +822,7 @@ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:26.6667px;font-family:'Linux Libertine O';-inkscape-font-specification:'Linux Libertine O, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:center;white-space:pre;shape-inside:url(#rect1915);display:inline;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1.88976;stroke-dasharray:none;stroke-opacity:1">Coq + id="tspan1">Rocq Coq extraction + id="tspan24">Rocq extraction Coq + id="tspan26">Rocq Coq extraction + id="tspan49">Rocq extraction Coq Mechanization + id="tspan69">Rocq Mechanization Coq Extraction + id="tspan71">Rocq Extraction contradiction, due to continuation *) easy. Qed. -End Match. \ No newline at end of file +End Match. diff --git a/mechanization/props/NodeProps.v b/mechanization/props/NodeProps.v index 842b6df..220c670 100644 --- a/mechanization/props/NodeProps.v +++ b/mechanization/props/NodeProps.v @@ -1,4 +1,4 @@ -From Coq Require Import List Program.Equality PeanoNat. +From Stdlib Require Import List Program.Equality PeanoNat. From Warblre Require Import List Result Base Patterns Node. Import Patterns. @@ -342,4 +342,3 @@ Section Induction. forall r ctx, Root root (r, ctx) -> P (r, ctx). Proof. induction r; try eauto. Qed. End Induction. - diff --git a/mechanization/props/StrictlyNullable.v b/mechanization/props/StrictlyNullable.v index 248f411..e545899 100644 --- a/mechanization/props/StrictlyNullable.v +++ b/mechanization/props/StrictlyNullable.v @@ -1,4 +1,4 @@ -From Coq Require Import PeanoNat ZArith Bool Lia List. +From Stdlib Require Import PeanoNat ZArith Bool Lia List. From Warblre Require Import Tactics Focus Result Base Errors Patterns Node StaticSemantics Notation List Semantics Match EarlyErrors RegExpRecord. Import Notation. diff --git a/mechanization/spec/API.v b/mechanization/spec/API.v index 217b237..7e68a01 100644 --- a/mechanization/spec/API.v +++ b/mechanization/spec/API.v @@ -1,4 +1,4 @@ -From Coq Require Import Bool Nat. +From Stdlib Require Import Bool Nat. From Warblre Require Import Base Errors Result Return RegExpRecord Patterns Notation Semantics Frontend. Module API. diff --git a/mechanization/spec/Errors.v b/mechanization/spec/Errors.v index 4138e10..bebf842 100644 --- a/mechanization/spec/Errors.v +++ b/mechanization/spec/Errors.v @@ -4,8 +4,7 @@ From Warblre Require Import Typeclasses Result. (* Errors which occur during the early errors phase. *) Module SyntaxError. - (* Weird syntax to work around https://github.com/coq/coq/issues/7424 *) - Inductive type: let t := Type in t := + Inductive type: Type := | AssertionFailed. End SyntaxError. Notation SyntaxError := SyntaxError.type. @@ -16,8 +15,7 @@ Instance syntax_assertion_error: Result.AssertionError SyntaxError := { f := Syn (* Errors which occur during the compilation phase. *) Module CompileError. - (* Weird syntax to work around https://github.com/coq/coq/issues/7424 *) - Inductive type: let t := Type in t := + Inductive type: Type := | AssertionFailed. End CompileError. Notation CompileError := CompileError.type. @@ -41,4 +39,4 @@ Instance match_assertion_error: Result.AssertionError MatchError := { f := Match (* Shorthands *) Notation compile_assertion_failed := (Error CompileError.AssertionFailed). Notation out_of_fuel := (Error MatchError.OutOfFuel). -Notation match_assertion_failed := (Error MatchError.AssertionFailed). \ No newline at end of file +Notation match_assertion_failed := (Error MatchError.AssertionFailed). diff --git a/mechanization/spec/Frontend.v b/mechanization/spec/Frontend.v index d15aef4..e892299 100644 --- a/mechanization/spec/Frontend.v +++ b/mechanization/spec/Frontend.v @@ -1,4 +1,4 @@ -From Coq Require Import List ZArith. +From Stdlib Require Import List ZArith. From Warblre Require Import RegExpRecord Base Errors Notation Patterns Node StaticSemantics Semantics Result List Characters Return. Import Result.Notations. @@ -485,10 +485,7 @@ Section BuiltinExec. (*>> c. Let r be matcher(input, inputIndex). <<*) let! r:(option MatchState) =<< matcher input inputIndex in (*>> d. If r is failure, then <<*) - (* + LATER: change once fix is released +*) - (* + The more natural looking r == failure - Triggers https://github.com/coq/coq/issues/18358 with coq < 8.20 *) - if @EqDec.eq_dec _ eqdec_option r failure then + if r == failure then (*>> i. If sticky is true, then <<*) if sticky then (*>> 1. Perform ? Set(R, "lastIndex", +0𝔽, true). <<*) @@ -497,7 +494,7 @@ Section BuiltinExec. Success (Terminates (Null R)) else (*>> ii. Set lastIndex to AdvanceStringIndex(S, lastIndex, fullUnicode). <<*) - let lastIndex := @String.advanceStringIndex _ string_string S lastIndex in + let lastIndex := @String.advanceStringIndex _ Parameters.string_class S lastIndex in repeatloop lastIndex fuel' (*>> e. Else <<*) else diff --git a/mechanization/spec/Inst.v b/mechanization/spec/Inst.v index 4b0aaa7..9d7e6fd 100644 --- a/mechanization/spec/Inst.v +++ b/mechanization/spec/Inst.v @@ -1,6 +1,6 @@ From Warblre Require Import API. From Warblre Require Import Frontend. -From Coq Require Import Lia. +From Stdlib Require Import Lia. (* This is one instantiation of the alphabet that can be executed within Rocq. *) (* This encodes the ASCII alphabet *) @@ -184,7 +184,7 @@ Module NaiveEngineParameters <: API.EngineParameters. - apply ListSet.set_mem_correct2 with (Aeq_dec := Character.equal). auto. Qed. - Lemma range_seq: forall base l, List.List.Range.Nat.Length.range base l = Coq.Lists.List.seq base l. + Lemma range_seq: forall base l, List.List.Range.Nat.Length.range base l = Stdlib.Lists.List.seq base l. Proof. intros base l. revert base. @@ -344,7 +344,7 @@ End NaiveEngineParameters. (* We remove the fast engine, at least for now *) (* -From Coq Require Import OrdersEx MSetRBT. +From Stdlib Require Import OrdersEx MSetRBT. Module FastEngineParameters <: API.EngineParameters. Import RegExpRecord Numeric List ZArith Result. @@ -519,7 +519,7 @@ End FastEngineParameters. Module NaiveEngine := API.Engine (NaiveEngineParameters). (*Module FastEngine := API.Engine (NaiveEngineParameters).*) -Require Import Coq.Strings.Ascii Coq.Strings.String. +Require Import Stdlib.Strings.Ascii Stdlib.Strings.String. Open Scope string_scope. Import API.Patterns Result. @@ -528,16 +528,16 @@ Open Scope list_scope. Import NaiveEngine. (* Import FastEngine. *) -Definition get_success {S F} (r: Result S F) : match r with Success _ => S | Error _ => unit end := +Definition get_success {S F: Type} (r: Result S F) : match r with Success _ => S | Error _ => unit end := match r with | Success s => s | Error f => tt end. -Definition string_of_String (s: Coq.Strings.String.string) := +Definition string_of_String (s: Stdlib.Strings.String.string) := List.map Byte.to_nat (String.list_byte_of_string s). -Definition character_of_Ascii (a: Coq.Strings.Ascii.ascii) := +Definition character_of_Ascii (a: Stdlib.Strings.Ascii.ascii) := Byte.to_nat (byte_of_ascii a). Example flags := @@ -548,9 +548,10 @@ Notation "$ c" := (character_of_Ascii c) (at level 0). Notation "$$ s" := (string_of_String s) (at level 0). (* Hide the matching functions in the outputs below*) -Arguments Exotic {C S UP}%type_scope {H H0 H1} _ {_}. -Arguments Null {C S UP}%type_scope {H H0 H1} {_}. +Arguments Exotic {C S UP}%_type_scope {H H0 H1} _ {_}. +Arguments Null {C S UP}%_type_scope {H H0 H1} {_}. +(* Time Compute rmatch ! (Char $ "l") @@ -584,4 +585,4 @@ Time Compute (Quantified (Char $ "a") (Greedy Question)) (Quantified (Char $ "b") (Lazy Question)))) (Greedy Star)) - $$ "ab". + $$ "ab". *) diff --git a/mechanization/spec/Node.v b/mechanization/spec/Node.v index 08698db..43bb699 100644 --- a/mechanization/spec/Node.v +++ b/mechanization/spec/Node.v @@ -1,4 +1,4 @@ -From Coq Require Import List. +From Stdlib Require Import List. From Warblre Require Import Result Typeclasses Base Notation Patterns. (** + @@ -76,4 +76,4 @@ Section Zipper. End EqDec. End Zipper. Notation RegexContext := (list RegexContextLayer). -Notation RegexNode := (Regex * RegexContext)%type. \ No newline at end of file +Notation RegexNode := (Regex * RegexContext)%type. diff --git a/mechanization/spec/Notation.v b/mechanization/spec/Notation.v index 364af13..5734b99 100644 --- a/mechanization/spec/Notation.v +++ b/mechanization/spec/Notation.v @@ -1,4 +1,4 @@ -From Coq Require Import ZArith List. +From Stdlib Require Import ZArith List. From Warblre Require Import Typeclasses Result Numeric Characters Errors Parameters List. (** ## WILDCARD Sections diff --git a/mechanization/spec/Parameters.v b/mechanization/spec/Parameters.v index 8b61259..0edad35 100644 --- a/mechanization/spec/Parameters.v +++ b/mechanization/spec/Parameters.v @@ -1,5 +1,5 @@ From Warblre Require Import Result Typeclasses Numeric RegExpRecord. -From Coq Require Import List. +From Stdlib Require Import List. Import ListNotations. (** @@ -85,7 +85,7 @@ Module CharSet. (fun c0 => (Character.canonicalize rer c0) == c); (* Predicates and extra properties *) - (* Inspired by Coq.MSets.MSetInterface, unless specified otherwise *) + (* Inspired by Stdlib.MSets.MSetInterface, unless specified otherwise *) In: Character -> type -> Prop; Equal s1 s2 := forall c, In c s1 <-> In c s2; Empty s := forall c, ~In c s; @@ -356,9 +356,6 @@ Module Parameters. End Parameters. Notation Parameters := @Parameters.class. -(* Used in Frontend.v due to bug in coq kernel (see call site). LATER: remove once bug is fixed. *) -Definition string_string `{Parameters}: String.class Character := Parameters.string_class. - (* Some special characters used by the specification. *) Module Characters. Section main. Context `{specParameters: Parameters}. @@ -377,4 +374,4 @@ Module Characters. Section main. Definition digits: CharSet := CharSet.from_list Character.digits. Definition white_spaces: CharSet := CharSet.from_list Character.white_spaces. Definition ascii_word_characters: CharSet := CharSet.from_list Character.ascii_word_characters. -End main. End Characters. \ No newline at end of file +End main. End Characters. diff --git a/mechanization/spec/Patterns.v b/mechanization/spec/Patterns.v index 962cce3..9cc5e67 100644 --- a/mechanization/spec/Patterns.v +++ b/mechanization/spec/Patterns.v @@ -1,4 +1,4 @@ -From Coq Require Import List Program.Equality PeanoNat. +From Stdlib Require Import List Program.Equality PeanoNat. From Warblre Require Import List Result Typeclasses Notation Numeric Characters Parameters. (** ## WILDCARD Sections diff --git a/mechanization/spec/Semantics.v b/mechanization/spec/Semantics.v index aa68188..00fbb9f 100644 --- a/mechanization/spec/Semantics.v +++ b/mechanization/spec/Semantics.v @@ -1,4 +1,4 @@ -From Coq Require Import PeanoNat ZArith Bool Lia Program.Equality List Program.Wf. +From Stdlib Require Import PeanoNat ZArith Bool Lia Program.Equality List Program.Wf. From Warblre Require Import RegExpRecord Tactics Focus Result Base Patterns Errors StaticSemantics Node Notation List Typeclasses. Import Result.Notations. @@ -469,7 +469,7 @@ Module Semantics. Section main. parenIndex (a non-negative integer), and parenCount (a non-negative integer) and returns a MatchResult. It performs the following steps when called: <<*) - (* + Coq wants to make sure the function will terminate; we do so by bounding recursion by an arbitrary fuel amount +*) + (* + Rocq wants to make sure the function will terminate; we do so by bounding recursion by an arbitrary fuel amount +*) Fixpoint repeatMatcher' (m: Matcher) (min: non_neg_integer) (max: non_neg_integer_or_inf) (greedy: bool) (x: MatchState) (c: MatcherContinuation) (parenIndex parenCount: non_neg_integer) (fuel: nat): MatchResult := match fuel with | 0 => out_of_fuel diff --git a/mechanization/spec/StaticSemantics.v b/mechanization/spec/StaticSemantics.v index 8da9b36..11a64ec 100644 --- a/mechanization/spec/StaticSemantics.v +++ b/mechanization/spec/StaticSemantics.v @@ -1,4 +1,4 @@ -From Coq Require Import PeanoNat List Bool. +From Stdlib Require Import PeanoNat List Bool. From Warblre Require Import Result List Base Errors Result Patterns Node NodeProps Typeclasses. Import Coercions. diff --git a/mechanization/spec/base/Base.v b/mechanization/spec/base/Base.v index caea97b..8f3a331 100644 --- a/mechanization/spec/base/Base.v +++ b/mechanization/spec/base/Base.v @@ -1,4 +1,4 @@ -From Coq Require Import ZArith Lia List ListSet Bool. +From Stdlib Require Import ZArith Lia List ListSet Bool. From Warblre Require Import Tactics List Result. From Warblre Require Export Parameters. @@ -61,4 +61,4 @@ Notation "m 'is' 'not' p" := (match m with | p => false | _ => true end) (at lev Inductive Direction := | forward | backward. -#[refine] Instance eqdec_Direction: EqDec Direction := {}. decide equality. Defined. \ No newline at end of file +#[refine] Instance eqdec_Direction: EqDec Direction := {}. decide equality. Defined. diff --git a/mechanization/spec/base/Characters.v b/mechanization/spec/base/Characters.v index 0457225..b28b9d6 100644 --- a/mechanization/spec/base/Characters.v +++ b/mechanization/spec/base/Characters.v @@ -1,4 +1,4 @@ -From Coq Require Import PeanoNat List ListSet Structures.OrderedType FSets.FSetAVL NArith Bool. +From Stdlib Require Import PeanoNat List ListSet Structures.OrderedType FSets.FSetAVL NArith Bool. From Warblre Require Import RegExpRecord Tactics List Result Numeric Typeclasses. Import Result.Notations. diff --git a/mechanization/spec/base/Coercions.v b/mechanization/spec/base/Coercions.v index 23559db..00dad8f 100644 --- a/mechanization/spec/base/Coercions.v +++ b/mechanization/spec/base/Coercions.v @@ -1,4 +1,4 @@ -From Coq Require Import ZArith. +From Stdlib Require Import ZArith. From Warblre Require Import Result Numeric Characters Patterns Notation Parameters. Set Warnings "-uniform-inheritance". @@ -45,4 +45,4 @@ Module Coercions. End Coercions. #[export] -Hint Unfold Coercions.wrap_bool Coercions.wrap_list_Character Coercions.wrap_option Coercions.wrap_Result Coercions.wrap_Matcher Coercions.wrap_CharSet: result_wrappers. \ No newline at end of file +Hint Unfold Coercions.wrap_bool Coercions.wrap_list_Character Coercions.wrap_option Coercions.wrap_Result Coercions.wrap_Matcher Coercions.wrap_CharSet: result_wrappers. diff --git a/mechanization/spec/base/Numeric.v b/mechanization/spec/base/Numeric.v index a116599..3e450f3 100644 --- a/mechanization/spec/base/Numeric.v +++ b/mechanization/spec/base/Numeric.v @@ -1,4 +1,4 @@ -From Coq Require Import ZArith Lia. +From Stdlib Require Import ZArith Lia. From Warblre Require Import Result. (** Numeric datatypes, operations and notations. *) @@ -123,4 +123,4 @@ Infix "!=?" := (fun l r => negb (Z.eqb l r)) (at level 70): Z_scope. Infix "?" := Z.gtb (at level 70): Z_scope. -Infix ">=?" := Z.geb (at level 70): Z_scope. \ No newline at end of file +Infix ">=?" := Z.geb (at level 70): Z_scope. diff --git a/mechanization/tactics/Focus.v b/mechanization/tactics/Focus.v index 5204c03..a13d22a 100644 --- a/mechanization/tactics/Focus.v +++ b/mechanization/tactics/Focus.v @@ -23,25 +23,26 @@ Inductive focus := | LetBound (f: focus). (** Grammar to write focuses. *) +(* TODO: the levels were changed to avoid factorization issues, but + I have not put enough thoughts into it to be sure these changes are fine. *) Declare Custom Entry focus. Notation "''" := e (e custom focus at level 99). Notation "'[]'" := Here (in custom focus at level 0). Notation "'(' f ')'" := f (in custom focus at level 0, f at level 99). Notation "'if' f 'then' '_' 'else' '_'" := (IteCond f) (in custom focus at level 99). -Notation "f '_'" := (AppL f) (in custom focus at level 50, left associativity). -Notation "'_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity). -Notation "f -> '_'" := (ArrowL f) (in custom focus at level 70, right associativity). -Notation "'_' -> f" := (ArrowR f) (in custom focus at level 70, right associativity). -Notation "'_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity). -Notation "'_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). -Notation "'_' '_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). -Notation "'_' '_' '_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). -Notation "'_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). -Notation "'_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). -Notation "'_' '_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). -Notation "'_' '_' '_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). -Notation "'_' '_' '_' '_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). -Notation "'_' '_' '_' '_' '_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 50, f at level 49, left associativity, only parsing). +Notation "f '->' '_'" := (ArrowL f) (in custom focus at level 70, right associativity). +Notation "'_' '->' f" := (ArrowR f) (in custom focus at level 70, right associativity). +Notation "f '_'" := (AppL f) (in custom focus at level 70, no associativity). +Notation "'_' f" := (AppR f) (in custom focus at level 70, no associativity). +Notation "'_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). +Notation "'_' '_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). +Notation "'_' '_' '_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). +Notation "'_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). +Notation "'_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). +Notation "'_' '_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). +Notation "'_' '_' '_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). +Notation "'_' '_' '_' '_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). +Notation "'_' '_' '_' '_' '_' '_' '_' '_' '_' '_' f" := (AppR f) (in custom focus at level 70, no associativity, only parsing). (** Internal implementation *) Local Fixpoint focus_insert (f inserted: focus) := match f with diff --git a/mechanization/tactics/Retrieve.v b/mechanization/tactics/Retrieve.v index 9081584..3c8c9f6 100644 --- a/mechanization/tactics/Retrieve.v +++ b/mechanization/tactics/Retrieve.v @@ -1,13 +1,6 @@ Require Import Ltac2.Ltac2. From Ltac2 Require Import Control Pattern List. -(* LATER: - once updated to a newer version (8.20?) supporting https://github.com/coq/coq/pull/18690, - remove and use builtin. -*) -Ltac2 numgoals (_: unit): int := - 1. - (** A tactic to retrieve an hypothesis by the shape of its type. *) Ltac2 retrieve (pat: pattern) (into: ident): unit := let hyp_patterns := (None, (Pattern.MatchPattern, pat)) :: [] in @@ -17,4 +10,4 @@ Ltac2 retrieve (pat: pattern) (into: ident): unit := if Bool.neg (Int.equal (numgoals ()) 1) then Control.throw_invalid_argument "Multiple hypothese match the pattern" else (); let h := Array.get a 0 in Std.rename ((h, into) :: []). -Ltac2 Notation "retrieve" pat(pattern) "as" into(ident) := retrieve pat into. \ No newline at end of file +Ltac2 Notation "retrieve" pat(pattern) "as" into(ident) := retrieve pat into. diff --git a/mechanization/tactics/Tactics.v b/mechanization/tactics/Tactics.v index ea98cc2..01e5720 100644 --- a/mechanization/tactics/Tactics.v +++ b/mechanization/tactics/Tactics.v @@ -1,4 +1,4 @@ -From Coq Require Import Program.Tactics Bool.Bool ZArith. +From Stdlib Require Import Program.Tactics Bool.Bool ZArith. Tactic Notation "delta" reference(id) := cbv delta [ id ]. Tactic Notation "delta" reference(id) "in" hyp(h) := cbv delta [ id ] in h. @@ -34,8 +34,8 @@ Tactic Notation "exApplyW" hyp(H) hyp(w) "as" simple_intropattern(As) := Ltac clean_injection H := injection H; clear H; intros. Ltac bookkeeper := repeat ( - Coq.Program.Tactics.destruct_conjs - || Coq.Program.Tactics.clear_dups + destruct_conjs + || clear_dups || subst || lazymatch goal with | [ H: _ = _ |- _ ] => clean_injection H || discriminate H @@ -209,4 +209,4 @@ end. Tactic Notation "fforward" hyp(H) := fforward_impl H idtac. Tactic Notation "fforward" hyp(H) "as" simple_intropattern(I) := fforward_impl H idtac; destruct H as I. Tactic Notation "fforward" hyp(H) "by" tactic(t) := fforward_impl H t. -Tactic Notation "fforward" hyp(H) "as" simple_intropattern(I) "by" tactic(t) := fforward_impl H t; destruct H as I. \ No newline at end of file +Tactic Notation "fforward" hyp(H) "as" simple_intropattern(I) "by" tactic(t) := fforward_impl H t; destruct H as I. diff --git a/mechanization/utils/List.v b/mechanization/utils/List.v index c386071..62eb0d5 100644 --- a/mechanization/utils/List.v +++ b/mechanization/utils/List.v @@ -1,4 +1,4 @@ -From Coq Require Import ZArith Lia List Bool. +From Stdlib Require Import ZArith Lia List Bool. From Warblre Require Import Tactics Focus Result. Import Result.Notations. @@ -49,7 +49,7 @@ Module List. Proof. intros l1 l2 p12 p21 Eq_l1 Eq_l2. pose proof (@f_equal _ _ (@length _) _ _ Eq_l1). pose proof (@f_equal _ _ (@length _) _ _ Eq_l2). - rewrite -> app_length in *. + rewrite -> length_app in *. assert (length p12 = 0)%nat as Eq_p12 by lia. assert (length p21 = 0)%nat as Eq_p21 by lia. rewrite -> length_zero_iff_nil in *. subst. reflexivity. Qed. @@ -748,4 +748,4 @@ Module List. End Bounds. End Int. End Range. -End List. \ No newline at end of file +End List. diff --git a/mechanization/utils/Typeclasses.v b/mechanization/utils/Typeclasses.v index 94134cf..1726a01 100644 --- a/mechanization/utils/Typeclasses.v +++ b/mechanization/utils/Typeclasses.v @@ -1,5 +1,5 @@ From Warblre Require Import Retrieve. -From Coq Require Import ZArith Program.Equality Lia. +From Stdlib Require Import ZArith Program.Equality Lia. Local Close Scope nat. @@ -36,6 +36,5 @@ Instance eqdec_bool: EqDec bool := { eq_dec := Bool.bool_dec }. Instance eqdec_nat: EqDec nat := { eq_dec := Nat.eq_dec }. #[refine] Instance eqdec_positive: EqDec positive := {}. decide equality. Defined. #[refine] Instance eqdec_Z: EqDec Z := {}. decide equality; apply EqDec.eq_dec. Defined. -(* LATER: The cost (10) was needed at some point to avoid stack overflows when resolving EqDec in some theorems (e.g. EarlyErrors.groupSpecifiersThatMatch_singleton). *) -#[refine] Instance eqdec_option {T: Type} `{EqDec T}: EqDec (option T) | 10 := {}. decide equality; apply EqDec.eq_dec. Defined. -#[refine] Instance eqdec_list {T: Type} `{EqDec T}: EqDec (list T) | 10 := {}. decide equality; apply EqDec.eq_dec. Defined. +#[refine] Instance eqdec_option {T: Type} `{EqDec T}: EqDec (option T) := {}. decide equality; apply EqDec.eq_dec. Defined. +#[refine] Instance eqdec_list {T: Type} `{EqDec T}: EqDec (list T) := {}. decide equality; apply EqDec.eq_dec. Defined. diff --git a/package-lock.json b/package-lock.json index 21d32fa..a961d15 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,5 +1,5 @@ { - "name": "warblre", + "name": "Warblre", "lockfileVersion": 3, "requires": true, "packages": { @@ -17,30 +17,29 @@ "resolved": "https://registry.npmjs.org/@discoveryjs/json-ext/-/json-ext-0.5.7.tgz", "integrity": "sha512-dBVuXR082gk3jsFp7Rd/JI4kytwGHecnCoTtXFb7DB6CNHp4rg5k1bhg0nWdLGLnOV71lmDzGQaLMy8iPLY0pw==", "dev": true, + "license": "MIT", "engines": { "node": ">=10.0.0" } }, "node_modules/@eslint-community/regexpp": { - "version": "4.11.1", - "resolved": "https://registry.npmjs.org/@eslint-community/regexpp/-/regexpp-4.11.1.tgz", - "integrity": "sha512-m4DVN9ZqskZoLU5GlWZadwDnYo3vAEydiUayB9widCl9ffWx2IvPnp6n3on5rJmziJSw9Bv+Z3ChDVdMwXCY8Q==", + "version": "4.12.2", + "resolved": "https://registry.npmjs.org/@eslint-community/regexpp/-/regexpp-4.12.2.tgz", + "integrity": "sha512-EriSTlt5OC9/7SXkRSCAhfSxxoSUgBm33OH+IkwbdpgoqsSsUg7y3uh+IICI/Qg4BBWr3U2i39RpmycbxMq4ew==", + "license": "MIT", "engines": { "node": "^12.0.0 || ^14.0.0 || >=16.0.0" } }, "node_modules/@jridgewell/gen-mapping": { - "version": "0.3.5", - "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.5.tgz", - "integrity": "sha512-IzL8ZoEDIBRWEzlCcRhOaCupYyN5gdIK+Q6fbFdPDg6HqX6jpkItn7DFIpW9LQzXG6Df9sA7+OKnq0qlz/GaQg==", + "version": "0.3.13", + "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.13.tgz", + "integrity": "sha512-2kkt/7niJ6MgEPxF0bYdQ6etZaA+fQvDcLKckhy1yIQOzaoKjBBjSj63/aLVjYE3qhRt5dvM+uUyfCg6UKCBbA==", "dev": true, + "license": "MIT", "dependencies": { - "@jridgewell/set-array": "^1.2.1", - "@jridgewell/sourcemap-codec": "^1.4.10", + "@jridgewell/sourcemap-codec": "^1.5.0", "@jridgewell/trace-mapping": "^0.3.24" - }, - "engines": { - "node": ">=6.0.0" } }, "node_modules/@jridgewell/resolve-uri": { @@ -48,209 +47,244 @@ "resolved": "https://registry.npmjs.org/@jridgewell/resolve-uri/-/resolve-uri-3.1.2.tgz", "integrity": "sha512-bRISgCIjP20/tbWSPWMEi54QVPRZExkuD9lJL+UIxUKtwVJA8wW1Trb1jMs1RFXo1CBTNZ/5hpC9QvmKWdopKw==", "dev": true, - "engines": { - "node": ">=6.0.0" - } - }, - "node_modules/@jridgewell/set-array": { - "version": "1.2.1", - "resolved": "https://registry.npmjs.org/@jridgewell/set-array/-/set-array-1.2.1.tgz", - "integrity": "sha512-R8gLRTZeyp03ymzP/6Lil/28tGeGEzhx1q2k703KGWRAI1VdvPIXdG70VJc2pAMw3NA6JKL5hhFu1sJX0Mnn/A==", - "dev": true, + "license": "MIT", "engines": { "node": ">=6.0.0" } }, "node_modules/@jridgewell/source-map": { - "version": "0.3.6", - "resolved": "https://registry.npmjs.org/@jridgewell/source-map/-/source-map-0.3.6.tgz", - "integrity": "sha512-1ZJTZebgqllO79ue2bm3rIGud/bOe0pP5BjSRCRxxYkEZS8STV7zN84UBbiYu7jy+eCKSnVIUgoWWE/tt+shMQ==", + "version": "0.3.11", + "resolved": "https://registry.npmjs.org/@jridgewell/source-map/-/source-map-0.3.11.tgz", + "integrity": "sha512-ZMp1V8ZFcPG5dIWnQLr3NSI1MiCU7UETdS/A0G8V/XWHvJv3ZsFqutJn1Y5RPmAPX6F3BiE397OqveU/9NCuIA==", "dev": true, + "license": "MIT", "dependencies": { "@jridgewell/gen-mapping": "^0.3.5", "@jridgewell/trace-mapping": "^0.3.25" } }, "node_modules/@jridgewell/sourcemap-codec": { - "version": "1.5.0", - "resolved": "https://registry.npmjs.org/@jridgewell/sourcemap-codec/-/sourcemap-codec-1.5.0.tgz", - "integrity": "sha512-gv3ZRaISU3fjPAgNsriBRqGWQL6quFx04YMPW/zD8XMLsU32mhCCbfbO6KZFLjvYpCZ8zyDEgqsgf+PwPaM7GQ==", - "dev": true + "version": "1.5.5", + "resolved": "https://registry.npmjs.org/@jridgewell/sourcemap-codec/-/sourcemap-codec-1.5.5.tgz", + "integrity": "sha512-cYQ9310grqxueWbl+WuIUIaiUaDcj7WOq5fVhEljNVgRfOUhY9fy2zTvfoqWsnebh8Sl70VScFbICvJnLKB0Og==", + "dev": true, + "license": "MIT" }, "node_modules/@jridgewell/trace-mapping": { - "version": "0.3.25", - "resolved": "https://registry.npmjs.org/@jridgewell/trace-mapping/-/trace-mapping-0.3.25.tgz", - "integrity": "sha512-vNk6aEwybGtawWmy/PzwnGDOjCkLWSD2wqvjGGAgOAwCGWySYXfYoxt00IJkTF+8Lb57DwOb3Aa0o9CApepiYQ==", + "version": "0.3.31", + "resolved": "https://registry.npmjs.org/@jridgewell/trace-mapping/-/trace-mapping-0.3.31.tgz", + "integrity": "sha512-zzNR+SdQSDJzc8joaeP8QQoCQr8NuYx2dIIytl1QeBEZHJ9uW6hebsrYgbz8hJwUQao3TWCMtmfV8Nu1twOLAw==", "dev": true, + "license": "MIT", "dependencies": { "@jridgewell/resolve-uri": "^3.1.0", "@jridgewell/sourcemap-codec": "^1.4.14" } }, + "node_modules/@types/eslint": { + "version": "9.6.1", + "resolved": "https://registry.npmjs.org/@types/eslint/-/eslint-9.6.1.tgz", + "integrity": "sha512-FXx2pKgId/WyYo2jXw63kk7/+TY7u7AziEJxJAnSFzHlqTAS3Ync6SvgYAN/k4/PQpnnVuzoMuVnByKK2qp0ag==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/estree": "*", + "@types/json-schema": "*" + } + }, + "node_modules/@types/eslint-scope": { + "version": "3.7.7", + "resolved": "https://registry.npmjs.org/@types/eslint-scope/-/eslint-scope-3.7.7.tgz", + "integrity": "sha512-MzMFlSLBqNF2gcHWO0G1vP/YQyfvrxZ0bF+u7mzUdZ1/xK4A4sru+nraZz5i3iEIk1l1uyicaDVTB4QbbEkAYg==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/eslint": "*", + "@types/estree": "*" + } + }, "node_modules/@types/estree": { - "version": "1.0.6", - "resolved": "https://registry.npmjs.org/@types/estree/-/estree-1.0.6.tgz", - "integrity": "sha512-AYnb1nQyY49te+VRAVgmzfcgjYS91mY5P0TKUDCLEM+gNnA+3T6rWITXRLYCpahpqSQbN5cE+gHpnPyXjHWxcw==", - "dev": true + "version": "1.0.8", + "resolved": "https://registry.npmjs.org/@types/estree/-/estree-1.0.8.tgz", + "integrity": "sha512-dWHzHa2WqEXI/O1E9OjrocMTKJl2mSrEolh1Iomrv6U+JuNwaHXsXx9bLu5gG7BUWFIN0skIQJQ/L1rIex4X6w==", + "dev": true, + "license": "MIT" }, "node_modules/@types/json-schema": { "version": "7.0.15", "resolved": "https://registry.npmjs.org/@types/json-schema/-/json-schema-7.0.15.tgz", "integrity": "sha512-5+fP8P8MFNC+AyZCDxrB2pkZFPGzqQWUzpSeuuVLvm8VMcorNYavBqoFcxK8bQz4Qsbn4oUEEem4wDLfcysGHA==", - "dev": true + "dev": true, + "license": "MIT" }, "node_modules/@types/node": { - "version": "22.7.3", - "resolved": "https://registry.npmjs.org/@types/node/-/node-22.7.3.tgz", - "integrity": "sha512-qXKfhXXqGTyBskvWEzJZPUxSslAiLaB6JGP1ic/XTH9ctGgzdgYguuLP1C601aRTSDNlLb0jbKqXjZ48GNraSA==", + "version": "24.10.1", + "resolved": "https://registry.npmjs.org/@types/node/-/node-24.10.1.tgz", + "integrity": "sha512-GNWcUTRBgIRJD5zj+Tq0fKOJ5XZajIiBroOF0yvj2bSU1WvNdYS/dn9UxwsujGW4JX06dnHyjV2y9rRaybH0iQ==", "dev": true, + "license": "MIT", "dependencies": { - "undici-types": "~6.19.2" + "undici-types": "~7.16.0" } }, "node_modules/@webassemblyjs/ast": { - "version": "1.12.1", - "resolved": "https://registry.npmjs.org/@webassemblyjs/ast/-/ast-1.12.1.tgz", - "integrity": "sha512-EKfMUOPRRUTy5UII4qJDGPpqfwjOmZ5jeGFwid9mnoqIFK+e0vqoi1qH56JpmZSzEL53jKnNzScdmftJyG5xWg==", + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/@webassemblyjs/ast/-/ast-1.14.1.tgz", + "integrity": "sha512-nuBEDgQfm1ccRp/8bCQrx1frohyufl4JlbMMZ4P1wpeOfDhF6FQkxZJ1b/e+PLwr6X1Nhw6OLme5usuBWYBvuQ==", "dev": true, + "license": "MIT", "dependencies": { - "@webassemblyjs/helper-numbers": "1.11.6", - "@webassemblyjs/helper-wasm-bytecode": "1.11.6" + "@webassemblyjs/helper-numbers": "1.13.2", + "@webassemblyjs/helper-wasm-bytecode": "1.13.2" } }, "node_modules/@webassemblyjs/floating-point-hex-parser": { - "version": "1.11.6", - "resolved": "https://registry.npmjs.org/@webassemblyjs/floating-point-hex-parser/-/floating-point-hex-parser-1.11.6.tgz", - "integrity": "sha512-ejAj9hfRJ2XMsNHk/v6Fu2dGS+i4UaXBXGemOfQ/JfQ6mdQg/WXtwleQRLLS4OvfDhv8rYnVwH27YJLMyYsxhw==", - "dev": true + "version": "1.13.2", + "resolved": "https://registry.npmjs.org/@webassemblyjs/floating-point-hex-parser/-/floating-point-hex-parser-1.13.2.tgz", + "integrity": "sha512-6oXyTOzbKxGH4steLbLNOu71Oj+C8Lg34n6CqRvqfS2O71BxY6ByfMDRhBytzknj9yGUPVJ1qIKhRlAwO1AovA==", + "dev": true, + "license": "MIT" }, "node_modules/@webassemblyjs/helper-api-error": { - "version": "1.11.6", - "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-api-error/-/helper-api-error-1.11.6.tgz", - "integrity": "sha512-o0YkoP4pVu4rN8aTJgAyj9hC2Sv5UlkzCHhxqWj8butaLvnpdc2jOwh4ewE6CX0txSfLn/UYaV/pheS2Txg//Q==", - "dev": true + "version": "1.13.2", + "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-api-error/-/helper-api-error-1.13.2.tgz", + "integrity": "sha512-U56GMYxy4ZQCbDZd6JuvvNV/WFildOjsaWD3Tzzvmw/mas3cXzRJPMjP83JqEsgSbyrmaGjBfDtV7KDXV9UzFQ==", + "dev": true, + "license": "MIT" }, "node_modules/@webassemblyjs/helper-buffer": { - "version": "1.12.1", - "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-buffer/-/helper-buffer-1.12.1.tgz", - "integrity": "sha512-nzJwQw99DNDKr9BVCOZcLuJJUlqkJh+kVzVl6Fmq/tI5ZtEyWT1KZMyOXltXLZJmDtvLCDgwsyrkohEtopTXCw==", - "dev": true + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-buffer/-/helper-buffer-1.14.1.tgz", + "integrity": "sha512-jyH7wtcHiKssDtFPRB+iQdxlDf96m0E39yb0k5uJVhFGleZFoNw1c4aeIcVUPPbXUVJ94wwnMOAqUHyzoEPVMA==", + "dev": true, + "license": "MIT" }, "node_modules/@webassemblyjs/helper-numbers": { - "version": "1.11.6", - "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-numbers/-/helper-numbers-1.11.6.tgz", - "integrity": "sha512-vUIhZ8LZoIWHBohiEObxVm6hwP034jwmc9kuq5GdHZH0wiLVLIPcMCdpJzG4C11cHoQ25TFIQj9kaVADVX7N3g==", + "version": "1.13.2", + "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-numbers/-/helper-numbers-1.13.2.tgz", + "integrity": "sha512-FE8aCmS5Q6eQYcV3gI35O4J789wlQA+7JrqTTpJqn5emA4U2hvwJmvFRC0HODS+3Ye6WioDklgd6scJ3+PLnEA==", "dev": true, + "license": "MIT", "dependencies": { - "@webassemblyjs/floating-point-hex-parser": "1.11.6", - "@webassemblyjs/helper-api-error": "1.11.6", + "@webassemblyjs/floating-point-hex-parser": "1.13.2", + "@webassemblyjs/helper-api-error": "1.13.2", "@xtuc/long": "4.2.2" } }, "node_modules/@webassemblyjs/helper-wasm-bytecode": { - "version": "1.11.6", - "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-wasm-bytecode/-/helper-wasm-bytecode-1.11.6.tgz", - "integrity": "sha512-sFFHKwcmBprO9e7Icf0+gddyWYDViL8bpPjJJl0WHxCdETktXdmtWLGVzoHbqUcY4Be1LkNfwTmXOJUFZYSJdA==", - "dev": true + "version": "1.13.2", + "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-wasm-bytecode/-/helper-wasm-bytecode-1.13.2.tgz", + "integrity": "sha512-3QbLKy93F0EAIXLh0ogEVR6rOubA9AoZ+WRYhNbFyuB70j3dRdwH9g+qXhLAO0kiYGlg3TxDV+I4rQTr/YNXkA==", + "dev": true, + "license": "MIT" }, "node_modules/@webassemblyjs/helper-wasm-section": { - "version": "1.12.1", - "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-wasm-section/-/helper-wasm-section-1.12.1.tgz", - "integrity": "sha512-Jif4vfB6FJlUlSbgEMHUyk1j234GTNG9dBJ4XJdOySoj518Xj0oGsNi59cUQF4RRMS9ouBUxDDdyBVfPTypa5g==", + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/@webassemblyjs/helper-wasm-section/-/helper-wasm-section-1.14.1.tgz", + "integrity": "sha512-ds5mXEqTJ6oxRoqjhWDU83OgzAYjwsCV8Lo/N+oRsNDmx/ZDpqalmrtgOMkHwxsG0iI//3BwWAErYRHtgn0dZw==", "dev": true, + "license": "MIT", "dependencies": { - "@webassemblyjs/ast": "1.12.1", - "@webassemblyjs/helper-buffer": "1.12.1", - "@webassemblyjs/helper-wasm-bytecode": "1.11.6", - "@webassemblyjs/wasm-gen": "1.12.1" + "@webassemblyjs/ast": "1.14.1", + "@webassemblyjs/helper-buffer": "1.14.1", + "@webassemblyjs/helper-wasm-bytecode": "1.13.2", + "@webassemblyjs/wasm-gen": "1.14.1" } }, "node_modules/@webassemblyjs/ieee754": { - "version": "1.11.6", - "resolved": "https://registry.npmjs.org/@webassemblyjs/ieee754/-/ieee754-1.11.6.tgz", - "integrity": "sha512-LM4p2csPNvbij6U1f19v6WR56QZ8JcHg3QIJTlSwzFcmx6WSORicYj6I63f9yU1kEUtrpG+kjkiIAkevHpDXrg==", + "version": "1.13.2", + "resolved": "https://registry.npmjs.org/@webassemblyjs/ieee754/-/ieee754-1.13.2.tgz", + "integrity": "sha512-4LtOzh58S/5lX4ITKxnAK2USuNEvpdVV9AlgGQb8rJDHaLeHciwG4zlGr0j/SNWlr7x3vO1lDEsuePvtcDNCkw==", "dev": true, + "license": "MIT", "dependencies": { "@xtuc/ieee754": "^1.2.0" } }, "node_modules/@webassemblyjs/leb128": { - "version": "1.11.6", - "resolved": "https://registry.npmjs.org/@webassemblyjs/leb128/-/leb128-1.11.6.tgz", - "integrity": "sha512-m7a0FhE67DQXgouf1tbN5XQcdWoNgaAuoULHIfGFIEVKA6tu/edls6XnIlkmS6FrXAquJRPni3ZZKjw6FSPjPQ==", + "version": "1.13.2", + "resolved": "https://registry.npmjs.org/@webassemblyjs/leb128/-/leb128-1.13.2.tgz", + "integrity": "sha512-Lde1oNoIdzVzdkNEAWZ1dZ5orIbff80YPdHx20mrHwHrVNNTjNr8E3xz9BdpcGqRQbAEa+fkrCb+fRFTl/6sQw==", "dev": true, + "license": "Apache-2.0", "dependencies": { "@xtuc/long": "4.2.2" } }, "node_modules/@webassemblyjs/utf8": { - "version": "1.11.6", - "resolved": "https://registry.npmjs.org/@webassemblyjs/utf8/-/utf8-1.11.6.tgz", - "integrity": "sha512-vtXf2wTQ3+up9Zsg8sa2yWiQpzSsMyXj0qViVP6xKGCUT8p8YJ6HqI7l5eCnWx1T/FYdsv07HQs2wTFbbof/RA==", - "dev": true + "version": "1.13.2", + "resolved": "https://registry.npmjs.org/@webassemblyjs/utf8/-/utf8-1.13.2.tgz", + "integrity": "sha512-3NQWGjKTASY1xV5m7Hr0iPeXD9+RDobLll3T9d2AO+g3my8xy5peVyjSag4I50mR1bBSN/Ct12lo+R9tJk0NZQ==", + "dev": true, + "license": "MIT" }, "node_modules/@webassemblyjs/wasm-edit": { - "version": "1.12.1", - "resolved": "https://registry.npmjs.org/@webassemblyjs/wasm-edit/-/wasm-edit-1.12.1.tgz", - "integrity": "sha512-1DuwbVvADvS5mGnXbE+c9NfA8QRcZ6iKquqjjmR10k6o+zzsRVesil54DKexiowcFCPdr/Q0qaMgB01+SQ1u6g==", + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/@webassemblyjs/wasm-edit/-/wasm-edit-1.14.1.tgz", + "integrity": "sha512-RNJUIQH/J8iA/1NzlE4N7KtyZNHi3w7at7hDjvRNm5rcUXa00z1vRz3glZoULfJ5mpvYhLybmVcwcjGrC1pRrQ==", "dev": true, + "license": "MIT", "dependencies": { - "@webassemblyjs/ast": "1.12.1", - "@webassemblyjs/helper-buffer": "1.12.1", - "@webassemblyjs/helper-wasm-bytecode": "1.11.6", - "@webassemblyjs/helper-wasm-section": "1.12.1", - "@webassemblyjs/wasm-gen": "1.12.1", - "@webassemblyjs/wasm-opt": "1.12.1", - "@webassemblyjs/wasm-parser": "1.12.1", - "@webassemblyjs/wast-printer": "1.12.1" + "@webassemblyjs/ast": "1.14.1", + "@webassemblyjs/helper-buffer": "1.14.1", + "@webassemblyjs/helper-wasm-bytecode": "1.13.2", + "@webassemblyjs/helper-wasm-section": "1.14.1", + "@webassemblyjs/wasm-gen": "1.14.1", + "@webassemblyjs/wasm-opt": "1.14.1", + "@webassemblyjs/wasm-parser": "1.14.1", + "@webassemblyjs/wast-printer": "1.14.1" } }, "node_modules/@webassemblyjs/wasm-gen": { - "version": "1.12.1", - "resolved": "https://registry.npmjs.org/@webassemblyjs/wasm-gen/-/wasm-gen-1.12.1.tgz", - "integrity": "sha512-TDq4Ojh9fcohAw6OIMXqiIcTq5KUXTGRkVxbSo1hQnSy6lAM5GSdfwWeSxpAo0YzgsgF182E/U0mDNhuA0tW7w==", + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/@webassemblyjs/wasm-gen/-/wasm-gen-1.14.1.tgz", + "integrity": "sha512-AmomSIjP8ZbfGQhumkNvgC33AY7qtMCXnN6bL2u2Js4gVCg8fp735aEiMSBbDR7UQIj90n4wKAFUSEd0QN2Ukg==", "dev": true, + "license": "MIT", "dependencies": { - "@webassemblyjs/ast": "1.12.1", - "@webassemblyjs/helper-wasm-bytecode": "1.11.6", - "@webassemblyjs/ieee754": "1.11.6", - "@webassemblyjs/leb128": "1.11.6", - "@webassemblyjs/utf8": "1.11.6" + "@webassemblyjs/ast": "1.14.1", + "@webassemblyjs/helper-wasm-bytecode": "1.13.2", + "@webassemblyjs/ieee754": "1.13.2", + "@webassemblyjs/leb128": "1.13.2", + "@webassemblyjs/utf8": "1.13.2" } }, "node_modules/@webassemblyjs/wasm-opt": { - "version": "1.12.1", - "resolved": "https://registry.npmjs.org/@webassemblyjs/wasm-opt/-/wasm-opt-1.12.1.tgz", - "integrity": "sha512-Jg99j/2gG2iaz3hijw857AVYekZe2SAskcqlWIZXjji5WStnOpVoat3gQfT/Q5tb2djnCjBtMocY/Su1GfxPBg==", + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/@webassemblyjs/wasm-opt/-/wasm-opt-1.14.1.tgz", + "integrity": "sha512-PTcKLUNvBqnY2U6E5bdOQcSM+oVP/PmrDY9NzowJjislEjwP/C4an2303MCVS2Mg9d3AJpIGdUFIQQWbPds0Sw==", "dev": true, + "license": "MIT", "dependencies": { - "@webassemblyjs/ast": "1.12.1", - "@webassemblyjs/helper-buffer": "1.12.1", - "@webassemblyjs/wasm-gen": "1.12.1", - "@webassemblyjs/wasm-parser": "1.12.1" + "@webassemblyjs/ast": "1.14.1", + "@webassemblyjs/helper-buffer": "1.14.1", + "@webassemblyjs/wasm-gen": "1.14.1", + "@webassemblyjs/wasm-parser": "1.14.1" } }, "node_modules/@webassemblyjs/wasm-parser": { - "version": "1.12.1", - "resolved": "https://registry.npmjs.org/@webassemblyjs/wasm-parser/-/wasm-parser-1.12.1.tgz", - "integrity": "sha512-xikIi7c2FHXysxXe3COrVUPSheuBtpcfhbpFj4gmu7KRLYOzANztwUU0IbsqvMqzuNK2+glRGWCEqZo1WCLyAQ==", + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/@webassemblyjs/wasm-parser/-/wasm-parser-1.14.1.tgz", + "integrity": "sha512-JLBl+KZ0R5qB7mCnud/yyX08jWFw5MsoalJ1pQ4EdFlgj9VdXKGuENGsiCIjegI1W7p91rUlcB/LB5yRJKNTcQ==", "dev": true, + "license": "MIT", "dependencies": { - "@webassemblyjs/ast": "1.12.1", - "@webassemblyjs/helper-api-error": "1.11.6", - "@webassemblyjs/helper-wasm-bytecode": "1.11.6", - "@webassemblyjs/ieee754": "1.11.6", - "@webassemblyjs/leb128": "1.11.6", - "@webassemblyjs/utf8": "1.11.6" + "@webassemblyjs/ast": "1.14.1", + "@webassemblyjs/helper-api-error": "1.13.2", + "@webassemblyjs/helper-wasm-bytecode": "1.13.2", + "@webassemblyjs/ieee754": "1.13.2", + "@webassemblyjs/leb128": "1.13.2", + "@webassemblyjs/utf8": "1.13.2" } }, "node_modules/@webassemblyjs/wast-printer": { - "version": "1.12.1", - "resolved": "https://registry.npmjs.org/@webassemblyjs/wast-printer/-/wast-printer-1.12.1.tgz", - "integrity": "sha512-+X4WAlOisVWQMikjbcvY2e0rwPsKQ9F688lksZhBcPycBBuii3O7m8FACbDMWDojpAqvjIncrG8J0XHKyQfVeA==", + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/@webassemblyjs/wast-printer/-/wast-printer-1.14.1.tgz", + "integrity": "sha512-kPSSXE6De1XOR820C90RIo2ogvZG+c3KiHzqUoO/F34Y2shGzesfqv7o57xrxovZJH/MetF5UjroJ/R/3isoiw==", "dev": true, + "license": "MIT", "dependencies": { - "@webassemblyjs/ast": "1.12.1", + "@webassemblyjs/ast": "1.14.1", "@xtuc/long": "4.2.2" } }, @@ -259,6 +293,7 @@ "resolved": "https://registry.npmjs.org/@webpack-cli/configtest/-/configtest-2.1.1.tgz", "integrity": "sha512-wy0mglZpDSiSS0XHrVR+BAdId2+yxPSoJW8fsna3ZpYSlufjvxnP4YbKTCBZnNIcGN4r6ZPXV55X4mYExOfLmw==", "dev": true, + "license": "MIT", "engines": { "node": ">=14.15.0" }, @@ -272,6 +307,7 @@ "resolved": "https://registry.npmjs.org/@webpack-cli/info/-/info-2.0.2.tgz", "integrity": "sha512-zLHQdI/Qs1UyT5UBdWNqsARasIA+AaF8t+4u2aS2nEpBQh2mWIVb8qAklq0eUENnC5mOItrIB4LiS9xMtph18A==", "dev": true, + "license": "MIT", "engines": { "node": ">=14.15.0" }, @@ -285,6 +321,7 @@ "resolved": "https://registry.npmjs.org/@webpack-cli/serve/-/serve-2.0.5.tgz", "integrity": "sha512-lqaoKnRYBdo1UgDX8uF24AfGMifWK19TxPmM5FHc2vAGxrJ/qtyUyFBWoY1tISZdelsQ5fBcOusifo5o5wSJxQ==", "dev": true, + "license": "MIT", "engines": { "node": ">=14.15.0" }, @@ -302,19 +339,23 @@ "version": "1.2.0", "resolved": "https://registry.npmjs.org/@xtuc/ieee754/-/ieee754-1.2.0.tgz", "integrity": "sha512-DX8nKgqcGwsc0eJSqYt5lwP4DH5FlHnmuWWBRy7X0NcaGR0ZtuyeESgMwTYVEtxmsNGY+qit4QYT/MIYTOTPeA==", - "dev": true + "dev": true, + "license": "BSD-3-Clause" }, "node_modules/@xtuc/long": { "version": "4.2.2", "resolved": "https://registry.npmjs.org/@xtuc/long/-/long-4.2.2.tgz", "integrity": "sha512-NuHqBY1PB/D8xU6s/thBgOAiAP7HOYDQ32+BFZILJ8ivkUkAHQnWfn6WhL79Owj1qmUnoN/YPhktdIoucipkAQ==", - "dev": true + "dev": true, + "license": "Apache-2.0" }, "node_modules/acorn": { - "version": "8.12.1", - "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.12.1.tgz", - "integrity": "sha512-tcpGyI9zbizT9JbV6oYE477V6mTlXvvi0T0G3SNIYE2apm/G5huBa1+K89VGeovbg+jycCrfhl3ADxErOuO6Jg==", + "version": "8.15.0", + "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.15.0.tgz", + "integrity": "sha512-NZyJarBfL7nWwIq+FDL6Zp/yHEhePMNnnJ0y3qfieCrmNvYct8uvtiV41UvlSe6apAfk0fY1FbWx+NwfmpvtTg==", "dev": true, + "license": "MIT", + "peer": true, "bin": { "acorn": "bin/acorn" }, @@ -322,44 +363,82 @@ "node": ">=0.4.0" } }, - "node_modules/acorn-import-attributes": { - "version": "1.9.5", - "resolved": "https://registry.npmjs.org/acorn-import-attributes/-/acorn-import-attributes-1.9.5.tgz", - "integrity": "sha512-n02Vykv5uA3eHGM/Z2dQrcD56kL8TyDb2p1+0P83PClMnC/nc+anbQRhIOWnSq4Ke/KvDPrY3C9hDtC/A3eHnQ==", + "node_modules/acorn-import-phases": { + "version": "1.0.4", + "resolved": "https://registry.npmjs.org/acorn-import-phases/-/acorn-import-phases-1.0.4.tgz", + "integrity": "sha512-wKmbr/DDiIXzEOiWrTTUcDm24kQ2vGfZQvM2fwg2vXqR5uW6aapr7ObPtj1th32b9u90/Pf4AItvdTh42fBmVQ==", "dev": true, + "license": "MIT", + "engines": { + "node": ">=10.13.0" + }, "peerDependencies": { - "acorn": "^8" + "acorn": "^8.14.0" } }, "node_modules/ajv": { - "version": "6.12.6", - "resolved": "https://registry.npmjs.org/ajv/-/ajv-6.12.6.tgz", - "integrity": "sha512-j3fVLgvTo527anyYyJOGTYJbG+vnnQYvE0m5mmkc1TK+nxAppkCLMIL0aZ4dblVCNoGShhm+kzE4ZUykBoMg4g==", + "version": "8.17.1", + "resolved": "https://registry.npmjs.org/ajv/-/ajv-8.17.1.tgz", + "integrity": "sha512-B/gBuNg5SiMTrPkC+A2+cW0RszwxYmn6VYxB/inlBStS5nx6xHIt/ehKRhIMhqusl7a8LjQoZnjCs5vhwxOQ1g==", "dev": true, + "license": "MIT", + "peer": true, "dependencies": { - "fast-deep-equal": "^3.1.1", - "fast-json-stable-stringify": "^2.0.0", - "json-schema-traverse": "^0.4.1", - "uri-js": "^4.2.2" + "fast-deep-equal": "^3.1.3", + "fast-uri": "^3.0.1", + "json-schema-traverse": "^1.0.0", + "require-from-string": "^2.0.2" }, "funding": { "type": "github", "url": "https://github.com/sponsors/epoberezkin" } }, + "node_modules/ajv-formats": { + "version": "2.1.1", + "resolved": "https://registry.npmjs.org/ajv-formats/-/ajv-formats-2.1.1.tgz", + "integrity": "sha512-Wx0Kx52hxE7C18hkMEggYlEifqWZtYaRgouJor+WMdPnQyEK13vgEWyVNup7SoeeoLMsr4kf5h6dOW11I15MUA==", + "dev": true, + "license": "MIT", + "dependencies": { + "ajv": "^8.0.0" + }, + "peerDependencies": { + "ajv": "^8.0.0" + }, + "peerDependenciesMeta": { + "ajv": { + "optional": true + } + } + }, "node_modules/ajv-keywords": { - "version": "3.5.2", - "resolved": "https://registry.npmjs.org/ajv-keywords/-/ajv-keywords-3.5.2.tgz", - "integrity": "sha512-5p6WTN0DdTGVQk6VjcEju19IgaHudalcfabD7yhDGeA6bcQnmL+CpveLJq/3hvfwd1aof6L386Ougkx6RfyMIQ==", + "version": "5.1.0", + "resolved": "https://registry.npmjs.org/ajv-keywords/-/ajv-keywords-5.1.0.tgz", + "integrity": "sha512-YCS/JNFAUyr5vAuhk1DWm1CBxRHW9LbJ2ozWeemrIqpbsqKjHVxYPyi5GC0rjZIT5JxJ3virVTS8wk4i/Z+krw==", "dev": true, + "license": "MIT", + "dependencies": { + "fast-deep-equal": "^3.1.3" + }, "peerDependencies": { - "ajv": "^6.9.1" + "ajv": "^8.8.2" + } + }, + "node_modules/baseline-browser-mapping": { + "version": "2.9.2", + "resolved": "https://registry.npmjs.org/baseline-browser-mapping/-/baseline-browser-mapping-2.9.2.tgz", + "integrity": "sha512-PxSsosKQjI38iXkmb3d0Y32efqyA0uW4s41u4IVBsLlWLhCiYNpH/AfNOVWRqCQBlD8TFJTz6OUWNd4DFJCnmw==", + "dev": true, + "license": "Apache-2.0", + "bin": { + "baseline-browser-mapping": "dist/cli.js" } }, "node_modules/browserslist": { - "version": "4.24.0", - "resolved": "https://registry.npmjs.org/browserslist/-/browserslist-4.24.0.tgz", - "integrity": "sha512-Rmb62sR1Zpjql25eSanFGEhAxcFwfA1K0GuQcLoaJBAcENegrQut3hYdhXFF1obQfiDyqIW/cLM5HSJ/9k884A==", + "version": "4.28.1", + "resolved": "https://registry.npmjs.org/browserslist/-/browserslist-4.28.1.tgz", + "integrity": "sha512-ZC5Bd0LgJXgwGqUknZY/vkUQ04r8NXnJZ3yYi4vDmSiZmC/pdSN0NbNRPxZpbtO4uAfDUAFffO8IZoM3Gj8IkA==", "dev": true, "funding": [ { @@ -375,11 +454,14 @@ "url": "https://github.com/sponsors/ai" } ], + "license": "MIT", + "peer": true, "dependencies": { - "caniuse-lite": "^1.0.30001663", - "electron-to-chromium": "^1.5.28", - "node-releases": "^2.0.18", - "update-browserslist-db": "^1.1.0" + "baseline-browser-mapping": "^2.9.0", + "caniuse-lite": "^1.0.30001759", + "electron-to-chromium": "^1.5.263", + "node-releases": "^2.0.27", + "update-browserslist-db": "^1.2.0" }, "bin": { "browserslist": "cli.js" @@ -392,12 +474,13 @@ "version": "1.1.2", "resolved": "https://registry.npmjs.org/buffer-from/-/buffer-from-1.1.2.tgz", "integrity": "sha512-E+XQCRwSbaaiChtv6k6Dwgc+bx+Bs6vuKJHHl5kox/BaKbhiXzqQOwK4cO22yElGp2OCmjwVhT3HmxgyPGnJfQ==", - "dev": true + "dev": true, + "license": "MIT" }, "node_modules/caniuse-lite": { - "version": "1.0.30001664", - "resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001664.tgz", - "integrity": "sha512-AmE7k4dXiNKQipgn7a2xg558IRqPN3jMQY/rOsbxDhrd0tyChwbITBfiwtnqz8bi2M5mIWbxAYBvk7W7QBUS2g==", + "version": "1.0.30001759", + "resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001759.tgz", + "integrity": "sha512-Pzfx9fOKoKvevQf8oCXoyNRQ5QyxJj+3O0Rqx2V5oxT61KGx8+n6hV/IUyJeifUci2clnmmKVpvtiqRzgiWjSw==", "dev": true, "funding": [ { @@ -412,13 +495,15 @@ "type": "github", "url": "https://github.com/sponsors/ai" } - ] + ], + "license": "CC-BY-4.0" }, "node_modules/chrome-trace-event": { "version": "1.0.4", "resolved": "https://registry.npmjs.org/chrome-trace-event/-/chrome-trace-event-1.0.4.tgz", "integrity": "sha512-rNjApaLzuwaOTjCiT8lSDdGN1APCiqkChLMJxJPWLunPAt5fy8xgU9/jNOchV84wfIxrA0lRQB7oCT8jrn/wrQ==", "dev": true, + "license": "MIT", "engines": { "node": ">=6.0" } @@ -428,6 +513,7 @@ "resolved": "https://registry.npmjs.org/clone-deep/-/clone-deep-4.0.1.tgz", "integrity": "sha512-neHB9xuzh/wk0dIHweyAXv2aPGZIVk3pLMe+/RNzINf17fe0OG96QroktYAUm7SM1PBnzTabaLboqqxDyMU+SQ==", "dev": true, + "license": "MIT", "dependencies": { "is-plain-object": "^2.0.4", "kind-of": "^6.0.2", @@ -441,19 +527,22 @@ "version": "2.0.20", "resolved": "https://registry.npmjs.org/colorette/-/colorette-2.0.20.tgz", "integrity": "sha512-IfEDxwoWIjkeXL1eXcDiow4UbKjhLdq6/EuSVR9GMN7KVH3r9gQ83e73hsz1Nd1T3ijd5xv1wcWRYO+D6kCI2w==", - "dev": true + "dev": true, + "license": "MIT" }, "node_modules/commander": { "version": "2.20.3", "resolved": "https://registry.npmjs.org/commander/-/commander-2.20.3.tgz", "integrity": "sha512-GpVkmM8vF2vQUkj2LvZmD35JxeJOLCwJ9cUkugyk2nuhbv3+mJvpLYYt+0+USMxE+oj+ey/lJEnhZw75x/OMcQ==", - "dev": true + "dev": true, + "license": "MIT" }, "node_modules/cross-spawn": { - "version": "7.0.3", - "resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-7.0.3.tgz", - "integrity": "sha512-iRDPJKUPVEND7dHPO8rkbOnPpyDygcDFtWjpeWNCgy8WP2rXcxXL8TskReQl6OrB2G7+UJrags1q15Fudc7G6w==", + "version": "7.0.6", + "resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-7.0.6.tgz", + "integrity": "sha512-uV2QOWP2nWzsy2aMp8aRibhi9dlzF5Hgh5SHaB9OiTGEyDTiJJyx0uy51QXdyWbtAHNua4XJzUKca3OzKUd3vA==", "dev": true, + "license": "MIT", "dependencies": { "path-key": "^3.1.0", "shebang-command": "^2.0.0", @@ -464,16 +553,18 @@ } }, "node_modules/electron-to-chromium": { - "version": "1.5.29", - "resolved": "https://registry.npmjs.org/electron-to-chromium/-/electron-to-chromium-1.5.29.tgz", - "integrity": "sha512-PF8n2AlIhCKXQ+gTpiJi0VhcHDb69kYX4MtCiivctc2QD3XuNZ/XIOlbGzt7WAjjEev0TtaH6Cu3arZExm5DOw==", - "dev": true + "version": "1.5.265", + "resolved": "https://registry.npmjs.org/electron-to-chromium/-/electron-to-chromium-1.5.265.tgz", + "integrity": "sha512-B7IkLR1/AE+9jR2LtVF/1/6PFhY5TlnEHnlrKmGk7PvkJibg5jr+mLXLLzq3QYl6PA1T/vLDthQPqIPAlS/PPA==", + "dev": true, + "license": "ISC" }, "node_modules/enhanced-resolve": { - "version": "5.17.1", - "resolved": "https://registry.npmjs.org/enhanced-resolve/-/enhanced-resolve-5.17.1.tgz", - "integrity": "sha512-LMHl3dXhTcfv8gM4kEzIUeTQ+7fpdA0l2tUf34BddXPkz2A5xJ5L/Pchd5BL6rdccM9QGvu0sWZzK1Z1t4wwyg==", + "version": "5.18.3", + "resolved": "https://registry.npmjs.org/enhanced-resolve/-/enhanced-resolve-5.18.3.tgz", + "integrity": "sha512-d4lC8xfavMeBjzGr2vECC3fsGXziXZQyJxD868h2M/mBI3PwAuODxAkLkq5HYuvrPYcUtiLzsTo8U3PgX3Ocww==", "dev": true, + "license": "MIT", "dependencies": { "graceful-fs": "^4.2.4", "tapable": "^2.2.0" @@ -483,10 +574,11 @@ } }, "node_modules/envinfo": { - "version": "7.14.0", - "resolved": "https://registry.npmjs.org/envinfo/-/envinfo-7.14.0.tgz", - "integrity": "sha512-CO40UI41xDQzhLB1hWyqUKgFhs250pNcGbyGKe1l/e4FSaI/+YE4IMG76GDt0In67WLPACIITC+sOi08x4wIvg==", + "version": "7.21.0", + "resolved": "https://registry.npmjs.org/envinfo/-/envinfo-7.21.0.tgz", + "integrity": "sha512-Lw7I8Zp5YKHFCXL7+Dz95g4CcbMEpgvqZNNq3AmlT5XAV6CgAAk6gyAMqn2zjw08K9BHfcNuKrMiCPLByGafow==", "dev": true, + "license": "MIT", "bin": { "envinfo": "dist/cli.js" }, @@ -495,16 +587,18 @@ } }, "node_modules/es-module-lexer": { - "version": "1.5.4", - "resolved": "https://registry.npmjs.org/es-module-lexer/-/es-module-lexer-1.5.4.tgz", - "integrity": "sha512-MVNK56NiMrOwitFB7cqDwq0CQutbw+0BvLshJSse0MUNU+y1FC3bUS/AQg7oUng+/wKrrki7JfmwtVHkVfPLlw==", - "dev": true + "version": "1.7.0", + "resolved": "https://registry.npmjs.org/es-module-lexer/-/es-module-lexer-1.7.0.tgz", + "integrity": "sha512-jEQoCwk8hyb2AZziIOLhDqpm5+2ww5uIE6lkO/6jcOCusfk6LhMHpXXfBLXTZ7Ydyt0j4VoUQv6uGNYbdW+kBA==", + "dev": true, + "license": "MIT" }, "node_modules/escalade": { "version": "3.2.0", "resolved": "https://registry.npmjs.org/escalade/-/escalade-3.2.0.tgz", "integrity": "sha512-WUj2qlxaQtO4g6Pq5c29GTcWGDyd8itL8zTlipgECz3JesAiiOKotd8JU6otB3PACgG6xkJUyVhboMS+bje/jA==", "dev": true, + "license": "MIT", "engines": { "node": ">=6" } @@ -514,6 +608,7 @@ "resolved": "https://registry.npmjs.org/eslint-scope/-/eslint-scope-5.1.1.tgz", "integrity": "sha512-2NxwbF/hZ0KpepYN0cNbo+FN6XoK7GaHlQhgx/hIZl6Va0bF45RQOOwhLIy8lQDbuCiadSLCBnH2CFYquit5bw==", "dev": true, + "license": "BSD-2-Clause", "dependencies": { "esrecurse": "^4.3.0", "estraverse": "^4.1.1" @@ -527,6 +622,7 @@ "resolved": "https://registry.npmjs.org/esrecurse/-/esrecurse-4.3.0.tgz", "integrity": "sha512-KmfKL3b6G+RXvP8N1vr3Tq1kL/oCFgn2NYXEtqP8/L3pKapUA4G8cFVaoF3SU323CD4XypR/ffioHmkti6/Tag==", "dev": true, + "license": "BSD-2-Clause", "dependencies": { "estraverse": "^5.2.0" }, @@ -539,6 +635,7 @@ "resolved": "https://registry.npmjs.org/estraverse/-/estraverse-5.3.0.tgz", "integrity": "sha512-MMdARuVEQziNTeJD8DgMqmhwR11BRQ/cBP+pLtYdSTnf3MIO8fFeiINEbX36ZdNlfU/7A9f3gUw49B3oQsvwBA==", "dev": true, + "license": "BSD-2-Clause", "engines": { "node": ">=4.0" } @@ -548,6 +645,7 @@ "resolved": "https://registry.npmjs.org/estraverse/-/estraverse-4.3.0.tgz", "integrity": "sha512-39nnKffWz8xN1BU/2c79n9nB9HDzo0niYUqx6xyqUnyoAnQyyWpOTdZEeiCch8BBu515t4wp9ZmgVfVhn9EBpw==", "dev": true, + "license": "BSD-2-Clause", "engines": { "node": ">=4.0" } @@ -557,6 +655,7 @@ "resolved": "https://registry.npmjs.org/events/-/events-3.3.0.tgz", "integrity": "sha512-mQw+2fkQbALzQ7V0MY0IqdnXNOeTtP4r0lN9z7AAawCXgqea7bDii20AYrIBrFd/Hx0M2Ocz6S111CaFkUcb0Q==", "dev": true, + "license": "MIT", "engines": { "node": ">=0.8.x" } @@ -565,19 +664,32 @@ "version": "3.1.3", "resolved": "https://registry.npmjs.org/fast-deep-equal/-/fast-deep-equal-3.1.3.tgz", "integrity": "sha512-f3qQ9oQy9j2AhBe/H9VC91wLmKBCCU/gDOnKNAYG5hswO7BLKj09Hc5HYNz9cGI++xlpDCIgDaitVs03ATR84Q==", - "dev": true + "dev": true, + "license": "MIT" }, - "node_modules/fast-json-stable-stringify": { - "version": "2.1.0", - "resolved": "https://registry.npmjs.org/fast-json-stable-stringify/-/fast-json-stable-stringify-2.1.0.tgz", - "integrity": "sha512-lhd/wF+Lk98HZoTCtlVraHtfh5XYijIjalXck7saUtuanSDyLMxnHhSXEDJqHxD7msR8D0uCmqlkwjCV8xvwHw==", - "dev": true + "node_modules/fast-uri": { + "version": "3.1.0", + "resolved": "https://registry.npmjs.org/fast-uri/-/fast-uri-3.1.0.tgz", + "integrity": "sha512-iPeeDKJSWf4IEOasVVrknXpaBV0IApz/gp7S2bb7Z4Lljbl2MGJRqInZiUrQwV16cpzw/D3S5j5Julj/gT52AA==", + "dev": true, + "funding": [ + { + "type": "github", + "url": "https://github.com/sponsors/fastify" + }, + { + "type": "opencollective", + "url": "https://opencollective.com/fastify" + } + ], + "license": "BSD-3-Clause" }, "node_modules/fastest-levenshtein": { "version": "1.0.16", "resolved": "https://registry.npmjs.org/fastest-levenshtein/-/fastest-levenshtein-1.0.16.tgz", "integrity": "sha512-eRnCtTTtGZFpQCwhJiUOuxPQWRXVKYDn0b2PeHfXL6/Zi53SLAzAHfVhVWK2AryC/WH05kGfxhFIPvTF0SXQzg==", "dev": true, + "license": "MIT", "engines": { "node": ">= 4.9.1" } @@ -587,6 +699,7 @@ "resolved": "https://registry.npmjs.org/find-up/-/find-up-4.1.0.tgz", "integrity": "sha512-PpOwAdQ/YlXQ2vj8a3h8IipDuYRi3wceVQQGYWxNINccq40Anw7BlsEXCMbt1Zt+OLA6Fq9suIpIWD0OsnISlw==", "dev": true, + "license": "MIT", "dependencies": { "locate-path": "^5.0.0", "path-exists": "^4.0.0" @@ -600,6 +713,7 @@ "resolved": "https://registry.npmjs.org/flat/-/flat-5.0.2.tgz", "integrity": "sha512-b6suED+5/3rTpUBdG1gupIl8MPFCAMA0QXwmljLhvCUKcUvdE4gWky9zpuGCcXHOsz4J9wPGNWq6OKpmIzz3hQ==", "dev": true, + "license": "BSD-3-Clause", "bin": { "flat": "cli.js" } @@ -609,6 +723,7 @@ "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.2.tgz", "integrity": "sha512-7XHNxH7qX9xG5mIwxkhumTox/MIRNcOgDrxWsMt2pAr23WHp6MrRlN7FBSFpCpr+oVO0F744iUgR82nJMfG2SA==", "dev": true, + "license": "MIT", "funding": { "url": "https://github.com/sponsors/ljharb" } @@ -617,19 +732,22 @@ "version": "0.4.1", "resolved": "https://registry.npmjs.org/glob-to-regexp/-/glob-to-regexp-0.4.1.tgz", "integrity": "sha512-lkX1HJXwyMcprw/5YUZc2s7DrpAiHB21/V+E1rHUrVNokkvB6bqMzT0VfV6/86ZNabt1k14YOIaT7nDvOX3Iiw==", - "dev": true + "dev": true, + "license": "BSD-2-Clause" }, "node_modules/graceful-fs": { "version": "4.2.11", "resolved": "https://registry.npmjs.org/graceful-fs/-/graceful-fs-4.2.11.tgz", "integrity": "sha512-RbJ5/jmFcNNCcDV5o9eTnBLJ/HszWV0P73bc+Ff4nS/rJj+YaS6IGyiOL0VoBYX+l1Wrl3k63h/KrH+nhJ0XvQ==", - "dev": true + "dev": true, + "license": "ISC" }, "node_modules/has-flag": { "version": "4.0.0", "resolved": "https://registry.npmjs.org/has-flag/-/has-flag-4.0.0.tgz", "integrity": "sha512-EykJT/Q1KjTWctppgIAgfSO0tKVuZUjhgMr17kqTumMl6Afv3EISleU7qZUzoXDFTAHTDC4NOoG/ZxU3EvlMPQ==", "dev": true, + "license": "MIT", "engines": { "node": ">=8" } @@ -639,6 +757,7 @@ "resolved": "https://registry.npmjs.org/hasown/-/hasown-2.0.2.tgz", "integrity": "sha512-0hJU9SCPvmMzIBdZFqNPXWa6dqh7WdH0cII9y+CyS8rG3nL48Bclra9HmKhVVUHyPWNH5Y7xDwAB7bfgSjkUMQ==", "dev": true, + "license": "MIT", "dependencies": { "function-bind": "^1.1.2" }, @@ -651,6 +770,7 @@ "resolved": "https://registry.npmjs.org/import-local/-/import-local-3.2.0.tgz", "integrity": "sha512-2SPlun1JUPWoM6t3F0dw0FkCF/jWY8kttcY4f599GLTSjh2OCuuhdTkJQsEcZzBqbXZGKMK2OqW1oZsjtf/gQA==", "dev": true, + "license": "MIT", "dependencies": { "pkg-dir": "^4.2.0", "resolve-cwd": "^3.0.0" @@ -670,15 +790,17 @@ "resolved": "https://registry.npmjs.org/interpret/-/interpret-3.1.1.tgz", "integrity": "sha512-6xwYfHbajpoF0xLW+iwLkhwgvLoZDfjYfoFNu8ftMoXINzwuymNLd9u/KmwtdT2GbR+/Cz66otEGEVVUHX9QLQ==", "dev": true, + "license": "MIT", "engines": { "node": ">=10.13.0" } }, "node_modules/is-core-module": { - "version": "2.15.1", - "resolved": "https://registry.npmjs.org/is-core-module/-/is-core-module-2.15.1.tgz", - "integrity": "sha512-z0vtXSwucUJtANQWldhbtbt7BnL0vxiFjIdDLAatwhDYty2bad6s+rijD6Ri4YuYJubLzIJLUidCh09e1djEVQ==", + "version": "2.16.1", + "resolved": "https://registry.npmjs.org/is-core-module/-/is-core-module-2.16.1.tgz", + "integrity": "sha512-UfoeMA6fIJ8wTYFEUjelnaGI67v6+N7qXJEvQuIGa99l4xsCruSYOVSQ0uPANn4dAzm8lkYPaKLrrijLq7x23w==", "dev": true, + "license": "MIT", "dependencies": { "hasown": "^2.0.2" }, @@ -694,6 +816,7 @@ "resolved": "https://registry.npmjs.org/is-plain-object/-/is-plain-object-2.0.4.tgz", "integrity": "sha512-h5PpgXkWitc38BBMYawTYMWJHFZJVnBquFE57xFpjB8pJFiF6gZ+bU+WyI/yqXiFR5mdLsgYNaPe8uao6Uv9Og==", "dev": true, + "license": "MIT", "dependencies": { "isobject": "^3.0.1" }, @@ -705,13 +828,15 @@ "version": "2.0.0", "resolved": "https://registry.npmjs.org/isexe/-/isexe-2.0.0.tgz", "integrity": "sha512-RHxMLp9lnKHGHRng9QFhRCMbYAcVpn69smSGcq3f36xjgVVWThj4qqLbTLlq7Ssj8B+fIQ1EuCEGI2lKsyQeIw==", - "dev": true + "dev": true, + "license": "ISC" }, "node_modules/isobject": { "version": "3.0.1", "resolved": "https://registry.npmjs.org/isobject/-/isobject-3.0.1.tgz", "integrity": "sha512-WhB9zCku7EGTj/HQQRz5aUQEUeoQZH2bWcltRErOpymJ4boYE6wL9Tbr23krRPSZ+C5zqNSrSw+Cc7sZZ4b7vg==", "dev": true, + "license": "MIT", "engines": { "node": ">=0.10.0" } @@ -721,6 +846,7 @@ "resolved": "https://registry.npmjs.org/jest-worker/-/jest-worker-27.5.1.tgz", "integrity": "sha512-7vuh85V5cdDofPyxn58nrPjBktZo0u9x1g8WtjQol+jZDaE+fhN+cIvTj11GndBnMnyfrUOG1sZQxCdjKh+DKg==", "dev": true, + "license": "MIT", "dependencies": { "@types/node": "*", "merge-stream": "^2.0.0", @@ -734,30 +860,38 @@ "version": "2.3.1", "resolved": "https://registry.npmjs.org/json-parse-even-better-errors/-/json-parse-even-better-errors-2.3.1.tgz", "integrity": "sha512-xyFwyhro/JEof6Ghe2iz2NcXoj2sloNsWr/XsERDK/oiPCfaNhl5ONfp+jQdAZRQQ0IJWNzH9zIZF7li91kh2w==", - "dev": true + "dev": true, + "license": "MIT" }, "node_modules/json-schema-traverse": { - "version": "0.4.1", - "resolved": "https://registry.npmjs.org/json-schema-traverse/-/json-schema-traverse-0.4.1.tgz", - "integrity": "sha512-xbbCH5dCYU5T8LcEhhuh7HJ88HXuW3qsI3Y0zOZFKfZEHcpWiHU/Jxzk629Brsab/mMiHQti9wMP+845RPe3Vg==", - "dev": true + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/json-schema-traverse/-/json-schema-traverse-1.0.0.tgz", + "integrity": "sha512-NM8/P9n3XjXhIZn1lLhkFaACTOURQXjWhV4BA/RnOv8xvgqtqpAX9IO4mRQxSx1Rlo4tqzeqb0sOlruaOy3dug==", + "dev": true, + "license": "MIT" }, "node_modules/kind-of": { "version": "6.0.3", "resolved": "https://registry.npmjs.org/kind-of/-/kind-of-6.0.3.tgz", "integrity": "sha512-dcS1ul+9tmeD95T+x28/ehLgd9mENa3LsvDTtzm3vyBEO7RPptvAD+t44WVXaUjTBRcrpFeFlC8WCruUR456hw==", "dev": true, + "license": "MIT", "engines": { "node": ">=0.10.0" } }, "node_modules/loader-runner": { - "version": "4.3.0", - "resolved": "https://registry.npmjs.org/loader-runner/-/loader-runner-4.3.0.tgz", - "integrity": "sha512-3R/1M+yS3j5ou80Me59j7F9IMs4PXs3VqRrm0TU3AbKPxlmpoY1TNscJV/oGJXo8qCatFGTfDbY6W6ipGOYXfg==", + "version": "4.3.1", + "resolved": "https://registry.npmjs.org/loader-runner/-/loader-runner-4.3.1.tgz", + "integrity": "sha512-IWqP2SCPhyVFTBtRcgMHdzlf9ul25NwaFx4wCEH/KjAXuuHY4yNjvPXsBokp8jCB936PyWRaPKUNh8NvylLp2Q==", "dev": true, + "license": "MIT", "engines": { "node": ">=6.11.5" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/webpack" } }, "node_modules/locate-path": { @@ -765,6 +899,7 @@ "resolved": "https://registry.npmjs.org/locate-path/-/locate-path-5.0.0.tgz", "integrity": "sha512-t7hw9pI+WvuwNJXwk5zVHpyhIqzg2qTlklJOf0mVxGSbe3Fp2VieZcduNYjaLDoy6p9uGpQEGWG87WpMKlNq8g==", "dev": true, + "license": "MIT", "dependencies": { "p-locate": "^4.1.0" }, @@ -776,13 +911,15 @@ "version": "2.0.0", "resolved": "https://registry.npmjs.org/merge-stream/-/merge-stream-2.0.0.tgz", "integrity": "sha512-abv/qOcuPfk3URPfDzmZU1LKmuw8kT+0nIHvKrKgFrwifol/doWcdA4ZqsWQ8ENrFKkd67Mfpo/LovbIUsbt3w==", - "dev": true + "dev": true, + "license": "MIT" }, "node_modules/mime-db": { "version": "1.52.0", "resolved": "https://registry.npmjs.org/mime-db/-/mime-db-1.52.0.tgz", "integrity": "sha512-sPU4uV7dYlvtWJxwwxHD0PuihVNiE7TyAbQ5SWxDCB9mUYvOgroQOwYQQOKPJ8CIbE+1ETVlOoK1UC2nU3gYvg==", "dev": true, + "license": "MIT", "engines": { "node": ">= 0.6" } @@ -792,6 +929,7 @@ "resolved": "https://registry.npmjs.org/mime-types/-/mime-types-2.1.35.tgz", "integrity": "sha512-ZDY+bPm5zTTF+YpCrAU9nK0UgICYPT0QtT1NZWFv4s++TNkcgVaT0g6+4R2uI4MjQjzysHB1zxuWL50hzaeXiw==", "dev": true, + "license": "MIT", "dependencies": { "mime-db": "1.52.0" }, @@ -803,19 +941,22 @@ "version": "2.6.2", "resolved": "https://registry.npmjs.org/neo-async/-/neo-async-2.6.2.tgz", "integrity": "sha512-Yd3UES5mWCSqR+qNT93S3UoYUkqAZ9lLg8a7g9rimsWmYGK8cVToA4/sF3RrshdyV3sAGMXVUmpMYOw+dLpOuw==", - "dev": true + "dev": true, + "license": "MIT" }, "node_modules/node-releases": { - "version": "2.0.18", - "resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.18.tgz", - "integrity": "sha512-d9VeXT4SJ7ZeOqGX6R5EM022wpL+eWPooLI+5UpWn2jCT1aosUQEhQP214x33Wkwx3JQMvIm+tIoVOdodFS40g==", - "dev": true + "version": "2.0.27", + "resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.27.tgz", + "integrity": "sha512-nmh3lCkYZ3grZvqcCH+fjmQ7X+H0OeZgP40OierEaAptX4XofMh5kwNbWh7lBduUzCcV/8kZ+NDLCwm2iorIlA==", + "dev": true, + "license": "MIT" }, "node_modules/p-limit": { "version": "2.3.0", "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", "dev": true, + "license": "MIT", "dependencies": { "p-try": "^2.0.0" }, @@ -831,6 +972,7 @@ "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-4.1.0.tgz", "integrity": "sha512-R79ZZ/0wAxKGu3oYMlz8jy/kbhsNrS7SKZ7PxEHBgJ5+F2mtFW2fK2cOtBh1cHYkQsbzFV7I+EoRKe6Yt0oK7A==", "dev": true, + "license": "MIT", "dependencies": { "p-limit": "^2.2.0" }, @@ -843,6 +985,7 @@ "resolved": "https://registry.npmjs.org/p-try/-/p-try-2.2.0.tgz", "integrity": "sha512-R4nPAVTAU0B9D35/Gk3uJf/7XYbQcyohSKdvAxIRSNghFl4e71hVoGnBNQz9cWaXxO2I10KTC+3jMdvvoKw6dQ==", "dev": true, + "license": "MIT", "engines": { "node": ">=6" } @@ -852,6 +995,7 @@ "resolved": "https://registry.npmjs.org/path-exists/-/path-exists-4.0.0.tgz", "integrity": "sha512-ak9Qy5Q7jYb2Wwcey5Fpvg2KoAc/ZIhLSLOSBmRmygPsGwkVVt0fZa0qrtMz+m6tJTAHfZQ8FnmB4MG4LWy7/w==", "dev": true, + "license": "MIT", "engines": { "node": ">=8" } @@ -861,6 +1005,7 @@ "resolved": "https://registry.npmjs.org/path-key/-/path-key-3.1.1.tgz", "integrity": "sha512-ojmeN0qd+y0jszEtoY48r0Peq5dwMEkIlCOu6Q5f41lfkswXuKtYrhgoTpLnyIcHm24Uhqx+5Tqm2InSwLhE6Q==", "dev": true, + "license": "MIT", "engines": { "node": ">=8" } @@ -869,19 +1014,22 @@ "version": "1.0.7", "resolved": "https://registry.npmjs.org/path-parse/-/path-parse-1.0.7.tgz", "integrity": "sha512-LDJzPVEEEPR+y48z93A0Ed0yXb8pAByGWo/k5YYdYgpY2/2EsOsksJrq7lOHxryrVOn1ejG6oAp8ahvOIQD8sw==", - "dev": true + "dev": true, + "license": "MIT" }, "node_modules/picocolors": { - "version": "1.1.0", - "resolved": "https://registry.npmjs.org/picocolors/-/picocolors-1.1.0.tgz", - "integrity": "sha512-TQ92mBOW0l3LeMeyLV6mzy/kWr8lkd/hp3mTg7wYK7zJhuBStmGMBG0BdeDZS/dZx1IukaX6Bk11zcln25o1Aw==", - "dev": true + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/picocolors/-/picocolors-1.1.1.tgz", + "integrity": "sha512-xceH2snhtb5M9liqDsmEw56le376mTZkEX/jEb/RxNFyegNul7eNslCXP9FDj/Lcu0X8KEyMceP2ntpaHrDEVA==", + "dev": true, + "license": "ISC" }, "node_modules/pkg-dir": { "version": "4.2.0", "resolved": "https://registry.npmjs.org/pkg-dir/-/pkg-dir-4.2.0.tgz", "integrity": "sha512-HRDzbaKjC+AOWVXxAU/x54COGeIv9eb+6CkDSQoNTt4XyWoIJvuPsXizxu/Fr23EiekbtZwmh1IcIG/l/a10GQ==", "dev": true, + "license": "MIT", "dependencies": { "find-up": "^4.0.0" }, @@ -889,20 +1037,12 @@ "node": ">=8" } }, - "node_modules/punycode": { - "version": "2.3.1", - "resolved": "https://registry.npmjs.org/punycode/-/punycode-2.3.1.tgz", - "integrity": "sha512-vYt7UD1U9Wg6138shLtLOvdAu+8DsC/ilFtEVHcH+wydcSpNE20AfSOduf6MkRFahL5FY7X1oU7nKVZFtfq8Fg==", - "dev": true, - "engines": { - "node": ">=6" - } - }, "node_modules/randombytes": { "version": "2.1.0", "resolved": "https://registry.npmjs.org/randombytes/-/randombytes-2.1.0.tgz", "integrity": "sha512-vYl3iOX+4CKUWuxGi9Ukhie6fsqXqS9FE2Zaic4tNFD2N2QQaXOMFbuKK4QmDHC0JO6B1Zp41J0LpT0oR68amQ==", "dev": true, + "license": "MIT", "dependencies": { "safe-buffer": "^5.1.0" } @@ -912,6 +1052,7 @@ "resolved": "https://registry.npmjs.org/rechoir/-/rechoir-0.8.0.tgz", "integrity": "sha512-/vxpCXddiX8NGfGO/mTafwjq4aFa/71pvamip0++IQk3zG8cbCj0fifNPrjjF1XMXUne91jL9OoxmdykoEtifQ==", "dev": true, + "license": "MIT", "dependencies": { "resolve": "^1.20.0" }, @@ -919,19 +1060,33 @@ "node": ">= 10.13.0" } }, + "node_modules/require-from-string": { + "version": "2.0.2", + "resolved": "https://registry.npmjs.org/require-from-string/-/require-from-string-2.0.2.tgz", + "integrity": "sha512-Xf0nWe6RseziFMu+Ap9biiUbmplq6S9/p+7w7YXP/JBHhrUDDUhwa+vANyubuqfZWTveU//DYVGsDG7RKL/vEw==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=0.10.0" + } + }, "node_modules/resolve": { - "version": "1.22.8", - "resolved": "https://registry.npmjs.org/resolve/-/resolve-1.22.8.tgz", - "integrity": "sha512-oKWePCxqpd6FlLvGV1VU0x7bkPmmCNolxzjMf4NczoDnQcIWrAF+cPtZn5i6n+RfD2d9i0tzpKnG6Yk168yIyw==", + "version": "1.22.11", + "resolved": "https://registry.npmjs.org/resolve/-/resolve-1.22.11.tgz", + "integrity": "sha512-RfqAvLnMl313r7c9oclB1HhUEAezcpLjz95wFH4LVuhk9JF/r22qmVP9AMmOU4vMX7Q8pN8jwNg/CSpdFnMjTQ==", "dev": true, + "license": "MIT", "dependencies": { - "is-core-module": "^2.13.0", + "is-core-module": "^2.16.1", "path-parse": "^1.0.7", "supports-preserve-symlinks-flag": "^1.0.0" }, "bin": { "resolve": "bin/resolve" }, + "engines": { + "node": ">= 0.4" + }, "funding": { "url": "https://github.com/sponsors/ljharb" } @@ -941,6 +1096,7 @@ "resolved": "https://registry.npmjs.org/resolve-cwd/-/resolve-cwd-3.0.0.tgz", "integrity": "sha512-OrZaX2Mb+rJCpH/6CpSqt9xFVpN++x01XnN2ie9g6P5/3xelLAkXWVADpdz1IHD/KFfEXyE6V0U01OQ3UO2rEg==", "dev": true, + "license": "MIT", "dependencies": { "resolve-from": "^5.0.0" }, @@ -953,6 +1109,7 @@ "resolved": "https://registry.npmjs.org/resolve-from/-/resolve-from-5.0.0.tgz", "integrity": "sha512-qYg9KP24dD5qka9J47d0aVky0N+b4fTU89LN9iDnjB5waksiC49rvMB0PrUJQGoTmH50XPiqOvAjDfaijGxYZw==", "dev": true, + "license": "MIT", "engines": { "node": ">=8" } @@ -975,17 +1132,20 @@ "type": "consulting", "url": "https://feross.org/support" } - ] + ], + "license": "MIT" }, "node_modules/schema-utils": { - "version": "3.3.0", - "resolved": "https://registry.npmjs.org/schema-utils/-/schema-utils-3.3.0.tgz", - "integrity": "sha512-pN/yOAvcC+5rQ5nERGuwrjLlYvLTbCibnZ1I7B1LaiAz9BRBlE9GMgE/eqV30P7aJQUf7Ddimy/RsbYO/GrVGg==", + "version": "4.3.3", + "resolved": "https://registry.npmjs.org/schema-utils/-/schema-utils-4.3.3.tgz", + "integrity": "sha512-eflK8wEtyOE6+hsaRVPxvUKYCpRgzLqDTb8krvAsRIwOGlHoSgYLgBXoubGgLd2fT41/OUYdb48v4k4WWHQurA==", "dev": true, + "license": "MIT", "dependencies": { - "@types/json-schema": "^7.0.8", - "ajv": "^6.12.5", - "ajv-keywords": "^3.5.2" + "@types/json-schema": "^7.0.9", + "ajv": "^8.9.0", + "ajv-formats": "^2.1.1", + "ajv-keywords": "^5.1.0" }, "engines": { "node": ">= 10.13.0" @@ -1000,6 +1160,7 @@ "resolved": "https://registry.npmjs.org/serialize-javascript/-/serialize-javascript-6.0.2.tgz", "integrity": "sha512-Saa1xPByTTq2gdeFZYLLo+RFE35NHZkAbqZeWNd3BpzppeVisAqpDjcp8dyf6uIvEqJRd46jemmyA4iFIeVk8g==", "dev": true, + "license": "BSD-3-Clause", "dependencies": { "randombytes": "^2.1.0" } @@ -1009,6 +1170,7 @@ "resolved": "https://registry.npmjs.org/shallow-clone/-/shallow-clone-3.0.1.tgz", "integrity": "sha512-/6KqX+GVUdqPuPPd2LxDDxzX6CAbjJehAAOKlNpqqUpAqPM6HeL8f+o3a+JsyGjn2lv0WY8UsTgUJjU9Ok55NA==", "dev": true, + "license": "MIT", "dependencies": { "kind-of": "^6.0.2" }, @@ -1021,6 +1183,7 @@ "resolved": "https://registry.npmjs.org/shebang-command/-/shebang-command-2.0.0.tgz", "integrity": "sha512-kHxr2zZpYtdmrN1qDjrrX/Z1rR1kG8Dx+gkpK1G4eXmvXswmcE1hTWBWYUzlraYw1/yZp6YuDY77YtvbN0dmDA==", "dev": true, + "license": "MIT", "dependencies": { "shebang-regex": "^3.0.0" }, @@ -1033,6 +1196,7 @@ "resolved": "https://registry.npmjs.org/shebang-regex/-/shebang-regex-3.0.0.tgz", "integrity": "sha512-7++dFhtcx3353uBaq8DDR4NuxBetBzC7ZQOhmTQInHEd6bSrXdiEyzCvG07Z44UYdLShWUyXt5M/yhz8ekcb1A==", "dev": true, + "license": "MIT", "engines": { "node": ">=8" } @@ -1042,6 +1206,7 @@ "resolved": "https://registry.npmjs.org/source-map/-/source-map-0.6.1.tgz", "integrity": "sha512-UjgapumWlbMhkBgzT7Ykc5YXUT46F0iKu8SGXq0bcwP5dz/h0Plj6enJqjz1Zbq2l5WaqYnrVbwWOWMyF3F47g==", "dev": true, + "license": "BSD-3-Clause", "engines": { "node": ">=0.10.0" } @@ -1051,6 +1216,7 @@ "resolved": "https://registry.npmjs.org/source-map-support/-/source-map-support-0.5.21.tgz", "integrity": "sha512-uBHU3L3czsIyYXKX88fdrGovxdSCoTGDRZ6SYXtSRxLZUzHg5P/66Ht6uoUlHu9EZod+inXhKo3qQgwXUT/y1w==", "dev": true, + "license": "MIT", "dependencies": { "buffer-from": "^1.0.0", "source-map": "^0.6.0" @@ -1061,6 +1227,7 @@ "resolved": "https://registry.npmjs.org/supports-color/-/supports-color-8.1.1.tgz", "integrity": "sha512-MpUEN2OodtUzxvKQl72cUF7RQ5EiHsGvSsVG0ia9c5RbWGL2CI4C7EpPS8UTBIplnlzZiNuV56w+FuNxy3ty2Q==", "dev": true, + "license": "MIT", "dependencies": { "has-flag": "^4.0.0" }, @@ -1076,6 +1243,7 @@ "resolved": "https://registry.npmjs.org/supports-preserve-symlinks-flag/-/supports-preserve-symlinks-flag-1.0.0.tgz", "integrity": "sha512-ot0WnXS9fgdkgIcePe6RHNk1WA8+muPa6cSjeR3V8K27q9BB1rTE3R1p7Hv0z1ZyAc8s6Vvv8DIyWf681MAt0w==", "dev": true, + "license": "MIT", "engines": { "node": ">= 0.4" }, @@ -1084,22 +1252,28 @@ } }, "node_modules/tapable": { - "version": "2.2.1", - "resolved": "https://registry.npmjs.org/tapable/-/tapable-2.2.1.tgz", - "integrity": "sha512-GNzQvQTOIP6RyTfE2Qxb8ZVlNmw0n88vp1szwWRimP02mnTsx3Wtn5qRdqY9w2XduFNUgvOwhNnQsjwCp+kqaQ==", + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/tapable/-/tapable-2.3.0.tgz", + "integrity": "sha512-g9ljZiwki/LfxmQADO3dEY1CbpmXT5Hm2fJ+QaGKwSXUylMybePR7/67YW7jOrrvjEgL1Fmz5kzyAjWVWLlucg==", "dev": true, + "license": "MIT", "engines": { "node": ">=6" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/webpack" } }, "node_modules/terser": { - "version": "5.34.0", - "resolved": "https://registry.npmjs.org/terser/-/terser-5.34.0.tgz", - "integrity": "sha512-y5NUX+U9HhVsK/zihZwoq4r9dICLyV2jXGOriDAVOeKhq3LKVjgJbGO90FisozXLlJfvjHqgckGmJFBb9KYoWQ==", + "version": "5.44.1", + "resolved": "https://registry.npmjs.org/terser/-/terser-5.44.1.tgz", + "integrity": "sha512-t/R3R/n0MSwnnazuPpPNVO60LX0SKL45pyl9YlvxIdkH0Of7D5qM2EVe+yASRIlY5pZ73nclYJfNANGWPwFDZw==", "dev": true, + "license": "BSD-2-Clause", "dependencies": { "@jridgewell/source-map": "^0.3.3", - "acorn": "^8.8.2", + "acorn": "^8.15.0", "commander": "^2.20.0", "source-map-support": "~0.5.20" }, @@ -1111,16 +1285,17 @@ } }, "node_modules/terser-webpack-plugin": { - "version": "5.3.10", - "resolved": "https://registry.npmjs.org/terser-webpack-plugin/-/terser-webpack-plugin-5.3.10.tgz", - "integrity": "sha512-BKFPWlPDndPs+NGGCr1U59t0XScL5317Y0UReNrHaw9/FwhPENlq6bfgs+4yPfyP51vqC1bQ4rp1EfXW5ZSH9w==", + "version": "5.3.14", + "resolved": "https://registry.npmjs.org/terser-webpack-plugin/-/terser-webpack-plugin-5.3.14.tgz", + "integrity": "sha512-vkZjpUjb6OMS7dhV+tILUW6BhpDR7P2L/aQSAv+Uwk+m8KATX9EccViHTJR2qDtACKPIYndLGCyl3FMo+r2LMw==", "dev": true, + "license": "MIT", "dependencies": { - "@jridgewell/trace-mapping": "^0.3.20", + "@jridgewell/trace-mapping": "^0.3.25", "jest-worker": "^27.4.5", - "schema-utils": "^3.1.1", - "serialize-javascript": "^6.0.1", - "terser": "^5.26.0" + "schema-utils": "^4.3.0", + "serialize-javascript": "^6.0.2", + "terser": "^5.31.1" }, "engines": { "node": ">= 10.13.0" @@ -1145,15 +1320,16 @@ } }, "node_modules/undici-types": { - "version": "6.19.8", - "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-6.19.8.tgz", - "integrity": "sha512-ve2KP6f/JnbPBFyobGHuerC9g1FYGn/F8n1LWTwNxCEzd6IfqTwUQcNXgEtmmQ6DlRrC1hrSrBnCZPokRrDHjw==", - "dev": true + "version": "7.16.0", + "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-7.16.0.tgz", + "integrity": "sha512-Zz+aZWSj8LE6zoxD+xrjh4VfkIG8Ya6LvYkZqtUQGJPZjYl53ypCaUwWqo7eI0x66KBGeRo+mlBEkMSeSZ38Nw==", + "dev": true, + "license": "MIT" }, "node_modules/update-browserslist-db": { - "version": "1.1.0", - "resolved": "https://registry.npmjs.org/update-browserslist-db/-/update-browserslist-db-1.1.0.tgz", - "integrity": "sha512-EdRAaAyk2cUE1wOf2DkEhzxqOQvFOoRJFNS6NeyJ01Gp2beMRpBAINjM2iDXE3KCuKhwnvHIQCJm6ThL2Z+HzQ==", + "version": "1.2.2", + "resolved": "https://registry.npmjs.org/update-browserslist-db/-/update-browserslist-db-1.2.2.tgz", + "integrity": "sha512-E85pfNzMQ9jpKkA7+TJAi4TJN+tBCuWh5rUcS/sv6cFi+1q9LYDwDI5dpUL0u/73EElyQ8d3TEaeW4sPedBqYA==", "dev": true, "funding": [ { @@ -1169,9 +1345,10 @@ "url": "https://github.com/sponsors/ai" } ], + "license": "MIT", "dependencies": { - "escalade": "^3.1.2", - "picocolors": "^1.0.1" + "escalade": "^3.2.0", + "picocolors": "^1.1.1" }, "bin": { "update-browserslist-db": "cli.js" @@ -1180,20 +1357,12 @@ "browserslist": ">= 4.21.0" } }, - "node_modules/uri-js": { - "version": "4.4.1", - "resolved": "https://registry.npmjs.org/uri-js/-/uri-js-4.4.1.tgz", - "integrity": "sha512-7rKUyy33Q1yc98pQ1DAmLtwX109F7TIfWlW1Ydo8Wl1ii1SeHieeh0HHfPeL2fMXK6z0s8ecKs9frCuLJvndBg==", - "dev": true, - "dependencies": { - "punycode": "^2.1.0" - } - }, "node_modules/watchpack": { - "version": "2.4.2", - "resolved": "https://registry.npmjs.org/watchpack/-/watchpack-2.4.2.tgz", - "integrity": "sha512-TnbFSbcOCcDgjZ4piURLCbJ3nJhznVh9kw6F6iokjiFPl8ONxe9A6nMDVXDiNbrSfLILs6vB07F7wLBrwPYzJw==", + "version": "2.4.4", + "resolved": "https://registry.npmjs.org/watchpack/-/watchpack-2.4.4.tgz", + "integrity": "sha512-c5EGNOiyxxV5qmTtAB7rbiXxi1ooX1pQKMLX/MIabJjRA0SJBQOjKF+KSVfHkr9U1cADPon0mRiVe/riyaiDUA==", "dev": true, + "license": "MIT", "dependencies": { "glob-to-regexp": "^0.4.1", "graceful-fs": "^4.1.2" @@ -1203,34 +1372,38 @@ } }, "node_modules/webpack": { - "version": "5.95.0", - "resolved": "https://registry.npmjs.org/webpack/-/webpack-5.95.0.tgz", - "integrity": "sha512-2t3XstrKULz41MNMBF+cJ97TyHdyQ8HCt//pqErqDvNjU9YQBnZxIHa11VXsi7F3mb5/aO2tuDxdeTPdU7xu9Q==", + "version": "5.103.0", + "resolved": "https://registry.npmjs.org/webpack/-/webpack-5.103.0.tgz", + "integrity": "sha512-HU1JOuV1OavsZ+mfigY0j8d1TgQgbZ6M+J75zDkpEAwYeXjWSqrGJtgnPblJjd/mAyTNQ7ygw0MiKOn6etz8yw==", "dev": true, + "license": "MIT", + "peer": true, "dependencies": { - "@types/estree": "^1.0.5", - "@webassemblyjs/ast": "^1.12.1", - "@webassemblyjs/wasm-edit": "^1.12.1", - "@webassemblyjs/wasm-parser": "^1.12.1", - "acorn": "^8.7.1", - "acorn-import-attributes": "^1.9.5", - "browserslist": "^4.21.10", + "@types/eslint-scope": "^3.7.7", + "@types/estree": "^1.0.8", + "@types/json-schema": "^7.0.15", + "@webassemblyjs/ast": "^1.14.1", + "@webassemblyjs/wasm-edit": "^1.14.1", + "@webassemblyjs/wasm-parser": "^1.14.1", + "acorn": "^8.15.0", + "acorn-import-phases": "^1.0.3", + "browserslist": "^4.26.3", "chrome-trace-event": "^1.0.2", - "enhanced-resolve": "^5.17.1", + "enhanced-resolve": "^5.17.3", "es-module-lexer": "^1.2.1", "eslint-scope": "5.1.1", "events": "^3.2.0", "glob-to-regexp": "^0.4.1", "graceful-fs": "^4.2.11", "json-parse-even-better-errors": "^2.3.1", - "loader-runner": "^4.2.0", + "loader-runner": "^4.3.1", "mime-types": "^2.1.27", "neo-async": "^2.6.2", - "schema-utils": "^3.2.0", - "tapable": "^2.1.1", - "terser-webpack-plugin": "^5.3.10", - "watchpack": "^2.4.1", - "webpack-sources": "^3.2.3" + "schema-utils": "^4.3.3", + "tapable": "^2.3.0", + "terser-webpack-plugin": "^5.3.11", + "watchpack": "^2.4.4", + "webpack-sources": "^3.3.3" }, "bin": { "webpack": "bin/webpack.js" @@ -1253,6 +1426,8 @@ "resolved": "https://registry.npmjs.org/webpack-cli/-/webpack-cli-5.1.4.tgz", "integrity": "sha512-pIDJHIEI9LR0yxHXQ+Qh95k2EvXpWzZ5l+d+jIo+RdSm9MiHfzazIxwwni/p7+x4eJZuvG1AJwgC4TNQ7NRgsg==", "dev": true, + "license": "MIT", + "peer": true, "dependencies": { "@discoveryjs/json-ext": "^0.5.0", "@webpack-cli/configtest": "^2.1.1", @@ -1298,6 +1473,7 @@ "resolved": "https://registry.npmjs.org/commander/-/commander-10.0.1.tgz", "integrity": "sha512-y4Mg2tXshplEbSGzx7amzPwKKOCGuoSRP/CjEdwwk0FOGlUbq6lKuoyDZTNZkmxHdJtp54hdfY/JUrdL7Xfdug==", "dev": true, + "license": "MIT", "engines": { "node": ">=14" } @@ -1307,6 +1483,7 @@ "resolved": "https://registry.npmjs.org/webpack-merge/-/webpack-merge-5.10.0.tgz", "integrity": "sha512-+4zXKdx7UnO+1jaN4l2lHVD+mFvnlZQP/6ljaJVb4SZiwIKeUnrT5l0gkT8z+n4hKpC+jpOv6O9R+gLtag7pSA==", "dev": true, + "license": "MIT", "dependencies": { "clone-deep": "^4.0.1", "flat": "^5.0.2", @@ -1317,10 +1494,11 @@ } }, "node_modules/webpack-sources": { - "version": "3.2.3", - "resolved": "https://registry.npmjs.org/webpack-sources/-/webpack-sources-3.2.3.tgz", - "integrity": "sha512-/DyMEOrDgLKKIG0fmvtz+4dUX/3Ghozwgm6iPp8KRhvn+eQf9+Q7GWxVNMk3+uCPWfdXYC4ExGBckIXdFEfH1w==", + "version": "3.3.3", + "resolved": "https://registry.npmjs.org/webpack-sources/-/webpack-sources-3.3.3.tgz", + "integrity": "sha512-yd1RBzSGanHkitROoPFd6qsrxt+oFhg/129YzheDGqeustzX0vTZJZsSsQjVQC4yzBQ56K55XU8gaNCtIzOnTg==", "dev": true, + "license": "MIT", "engines": { "node": ">=10.13.0" } @@ -1330,6 +1508,7 @@ "resolved": "https://registry.npmjs.org/which/-/which-2.0.2.tgz", "integrity": "sha512-BLI3Tl1TW3Pvl70l3yq3Y64i+awpwXqsGBYWkkqMtnbXgrMD+yj7rhW0kuEDxzJaYXGjEW5ogapKNMEKNMjibA==", "dev": true, + "license": "ISC", "dependencies": { "isexe": "^2.0.0" }, @@ -1344,7 +1523,8 @@ "version": "2.0.1", "resolved": "https://registry.npmjs.org/wildcard/-/wildcard-2.0.1.tgz", "integrity": "sha512-CC1bOL87PIWSBhDcTrdeLo6eGT7mCFtrg0uIJtqJUFyK+eJnzl8A1niH56uu7KMa5XFrtiV+AQuHO3n7DsHnLQ==", - "dev": true + "dev": true, + "license": "MIT" } } } diff --git a/specification_check/main.py b/specification_check/main.py index a18adef..7ca5d63 100644 --- a/specification_check/main.py +++ b/specification_check/main.py @@ -1,6 +1,6 @@ -from spec_merger.aligner import Aligner -from coq_parser import COQParser from ecma_parser import ECMAParser +from rocq_parser import ROCQParser +from spec_merger.aligner import Aligner from spec_merger.utils import Path @@ -9,13 +9,13 @@ def main(): files_to_exclude = [Path("../mechanization/spec/Node.v", False)] url = "https://262.ecma-international.org/14.0/" - coq_parser = COQParser(paths, files_to_exclude) - coq_parsed_page = coq_parser.get_parsed_page() + rocq_parser = ROCQParser(paths, files_to_exclude) + rocq_parsed_page = rocq_parser.get_parsed_page() ecma_parser_v14 = ECMAParser(url, parser_name="ECMAScript v14.0") ecma_parsed_page_v14 = ecma_parser_v14.get_parsed_page() a = Aligner() - result = a.align(coq_parsed_page.entries, ecma_parsed_page_v14.entries) + result = a.align(rocq_parsed_page.entries, ecma_parsed_page_v14.entries) text_result = result.to_text() print(text_result, end="") diff --git a/specification_check/coq_parser.py b/specification_check/rocq_parser.py similarity index 83% rename from specification_check/coq_parser.py rename to specification_check/rocq_parser.py index 38955bd..6bbb864 100644 --- a/specification_check/coq_parser.py +++ b/specification_check/rocq_parser.py @@ -1,20 +1,19 @@ import json - -from dataclasses import dataclass -from typing import List, Dict, Tuple -from alectryon.literate import coq_partition, Comment, StringView -import re import os +import re +from dataclasses import dataclass +from typing import Dict, List, Tuple -from spec_merger.utils import Path, ParserState, ParsedPage, Parser +from alectryon.literate import Comment, StringView, CoqParser from spec_merger.aligner_utils import Position from spec_merger.content_classes.dictionary import Dictionary from spec_merger.content_classes.string import String from spec_merger.content_classes.wildcard import WildCard +from spec_merger.utils import ParsedPage, Parser, ParserState, Path @dataclass(frozen=True) -class CoqLine: +class RocqLine: file_name: str line_number: int is_end_comment: bool = False @@ -35,7 +34,7 @@ def add_case(cases: dict[str, Dictionary | WildCard], left_key: str, right_key: @dataclass(frozen=True) -class CoqPosition(Position): +class RocqPosition(Position): file_positions: Dict[str, Tuple[int, int]] def html_str(self) -> str: @@ -48,8 +47,8 @@ def __hash__(self): return hash(self.html_str()) -class COQParser(Parser): - def __init__(self, files: List[Path], to_exclude: List[Path], parser_name: str = "COQ", +class ROCQParser(Parser): + def __init__(self, files: List[Path], to_exclude: List[Path], parser_name: str = "ROCQ", title_regex: str = r"(22\.2(?:\.[0-9]*)*)", spec_regex: str = r"^\(\*(\* )?>?>(.|\n)*?<<\*\)$", directive_regex: str = r"^\(\*(\* )?##(.|\n)*?##\*\)$", @@ -76,11 +75,11 @@ def __add_file(self, filename: str, files_dic: dict, all_filenames: list): if any([filename.startswith(excluded.uri) for excluded in self.to_exclude]): return with open(filename, "r") as f: - coq_file = f.read() - files_dic[filename] = coq_file + rocq_file = f.read() + files_dic[filename] = rocq_file all_filenames.append(filename) - def __get_coq_code(self) -> Tuple[Dict[str, str], List[str]]: + def __get_rocq_code(self) -> Tuple[Dict[str, str], List[str]]: files_dic: dict[str, str] = {} all_filenames: list[str] = [] for file in self.files: @@ -93,23 +92,23 @@ def __get_coq_code(self) -> Tuple[Dict[str, str], List[str]]: return files_dic, all_filenames - def __process_lines(self, coq_code, all_filenames, matcher: re.Pattern) -> list[tuple[str, CoqLine]]: + def __process_lines(self, rocq_code, all_filenames, matcher: re.Pattern) -> list[tuple[str, RocqLine]]: comments = [] for filename in all_filenames: - file = coq_code[filename] - partition = coq_partition(file) + file = rocq_code[filename] + partition = CoqParser(file).partition() for field in partition: if isinstance(field, Comment) and matcher.match(str(field.v)): - start_line_num = COQParser.__get_line_num(field.v) + start_line_num = ROCQParser.__get_line_num(field.v) for i, line in enumerate(str(field.v).splitlines()): - line = COQParser.__parse_line(line) + line = ROCQParser.__parse_line(line) if line != "": - comments.append((line, CoqLine(filename, start_line_num + i))) + comments.append((line, RocqLine(filename, start_line_num + i))) # avoid -1 at start, would have made no sense if len(comments) > 0: - comments.append(("", CoqLine(filename, -1, True))) + comments.append(("", RocqLine(filename, -1, True))) if len(comments) > 0: - comments.append(("", CoqLine(filename, -1, False, True))) + comments.append(("", RocqLine(filename, -1, False, True))) return comments @staticmethod @@ -134,7 +133,7 @@ def __merge_comments(section1: Dictionary, section2: Dictionary) -> Dictionary: section2["description"]) else section2["description"] description_second = section1["description"] if len(section1["description"]) <= len( section2["description"]) else section2["description"] - pos: tuple[CoqPosition, CoqPosition] = section1.position, section2.position + pos: tuple[RocqPosition, RocqPosition] = section1.position, section2.position new_files = {} old_files = (pos[0].file_positions, pos[1].file_positions) for filename in old_files[0].keys() | old_files[1].keys(): @@ -161,7 +160,7 @@ def __merge_comments(section1: Dictionary, section2: Dictionary) -> Dictionary: new_cases[case] = section1["cases"][case] else: new_cases[case] = section2["cases"][case] - return Dictionary(CoqPosition(new_files), {"title": title, "description": description_first + "\n" + + return Dictionary(RocqPosition(new_files), {"title": title, "description": description_first + "\n" + description_second, "cases": Dictionary(None, new_cases)}) @@ -179,7 +178,7 @@ def __get_comment_titles(self, comments) -> Dict[str, Dictionary]: for comment_index, comment in enumerate(comments): if res2 := self.any_title_regex.match(comment[0]): if current_block != "" and not section_to_be_thrown_away: - title_indices[current_block] = COQParser.__merge_comments( + title_indices[current_block] = ROCQParser.__merge_comments( self.__parse_subsection(comments[last_block_end:comment_index]), title_indices.get(current_block)) last_block_end = comment_index @@ -212,14 +211,14 @@ def __parse_subsection(self, comment_lines: List[str]) -> Dictionary: skip_until_end_file = False filenames = {} case_line_indices = [-1, -1] - for parsed_comment, coq_line in comment_lines: + for parsed_comment, rocq_line in comment_lines: # We are at the end of a comment - if coq_line.is_end_comment or coq_line.is_end_file: + if rocq_line.is_end_comment or rocq_line.is_end_file: match parser_state: case ParserState.BEFORE_START: parser_state = ParserState.READING_TITLE case ParserState.READING_TITLE: - if coq_line.is_end_comment: + if rocq_line.is_end_comment: parser_state = ParserState.READING_DESCRIPTION case ParserState.READING_DESCRIPTION: pass @@ -227,20 +226,20 @@ def __parse_subsection(self, comment_lines: List[str]) -> Dictionary: pass case ParserState.READING_WILDCARD: pass - if coq_line.is_end_file: + if rocq_line.is_end_file: skip_until_end_file = False continue if skip_until_end_file: continue # Get file name - filename = coq_line.file_name + filename = rocq_line.file_name # If not already in, add it and add its current line if filenames.get(filename) is None: - filenames[filename] = (coq_line.line_number, coq_line.line_number) + filenames[filename] = (rocq_line.line_number, rocq_line.line_number) # Otherwise update last line else: before_indices = filenames[filename] - added_index = coq_line.line_number + added_index = rocq_line.line_number new_indices = (min(before_indices[0], added_index), max(before_indices[1], added_index)) filenames[filename] = new_indices if parsed_comment.startswith("WILDCARD"): @@ -260,12 +259,12 @@ def __parse_subsection(self, comment_lines: List[str]) -> Dictionary: if self.case_regex.match(parsed_comment): parser_state = ParserState.READING_CASES if current_case != "": - case_pos = CoqPosition({coq_line.file_name: tuple(case_line_indices)}) + case_pos = RocqPosition({rocq_line.file_name: tuple(case_line_indices)}) for case_title in current_case_titles: add_case(cases, case_title[0], case_title[1], String(case_pos, current_case)) current_case_titles = [] - case_line_indices[0] = coq_line.line_number - case_line_indices[1] = coq_line.line_number + case_line_indices[0] = rocq_line.line_number + case_line_indices[1] = rocq_line.line_number match = self.case_regex.match(parsed_comment) current_case_titles.append([match.group(1), match.group(2)]) current_case = "" @@ -277,8 +276,8 @@ def __parse_subsection(self, comment_lines: List[str]) -> Dictionary: if self.algo_regex.match(parsed_comment): # If there is a start of an algorithm, but we are still building title, it means that there # is only one case in the subsection, and therefore we set its title to "" - case_line_indices[0] = coq_line.line_number - case_line_indices[1] = coq_line.line_number + case_line_indices[0] = rocq_line.line_number + case_line_indices[1] = rocq_line.line_number parser_state = ParserState.READING_CASES current_case = parsed_comment + "\n" if not current_case_titles: @@ -290,8 +289,8 @@ def __parse_subsection(self, comment_lines: List[str]) -> Dictionary: if self.algo_regex.match(parsed_comment): # If there is a start of an algorithm, but we are still building description, it means that # there is only one case in the subsection, and therefore we set its title to "" - case_line_indices[0] = coq_line.line_number - case_line_indices[1] = coq_line.line_number + case_line_indices[0] = rocq_line.line_number + case_line_indices[1] = rocq_line.line_number parser_state = ParserState.READING_CASES current_case = parsed_comment + "\n" if not current_case_titles: @@ -299,7 +298,7 @@ def __parse_subsection(self, comment_lines: List[str]) -> Dictionary: else: description += parsed_comment + " " case ParserState.READING_CASES: - case_line_indices[1] = coq_line.line_number + case_line_indices[1] = rocq_line.line_number if self.algo_regex.match(parsed_comment) or not in_case_title: if not current_case_titles: current_case_titles.append(["", ""]) @@ -308,11 +307,11 @@ def __parse_subsection(self, comment_lines: List[str]) -> Dictionary: elif in_case_title: current_case_titles[-1][1] += "\n" + parsed_comment if current_case != "": - case_pos = CoqPosition({comment_lines[-1][1].file_name: tuple(case_line_indices)}) + case_pos = RocqPosition({comment_lines[-1][1].file_name: tuple(case_line_indices)}) for case_title in current_case_titles: add_case(cases, case_title[0], case_title[1], String(case_pos, current_case)) cases_dict = Dictionary(None, cases) - return Dictionary(CoqPosition(filenames), {"title": String(None, title), + return Dictionary(RocqPosition(filenames), {"title": String(None, title), "description": String(None, description), "cases": cases_dict}) @@ -320,7 +319,7 @@ def __parse_directives(self, comments): state = ParserState.BEFORE_START acc = '' sections = [] - for comment, coq_line in comments: + for comment, rocq_line in comments: if comment == '': pass elif state == ParserState.BEFORE_START and comment.startswith('WILDCARD Sections'): @@ -330,7 +329,7 @@ def __parse_directives(self, comments): else: raise Exception("Unexpected directive part: '" + comment + "' (State: " + str(state) + ")") - if coq_line.is_end_comment: + if rocq_line.is_end_comment: sections += json.loads(acc) acc = '' state = ParserState.BEFORE_START @@ -338,11 +337,11 @@ def __parse_directives(self, comments): def get_parsed_page(self) -> ParsedPage: if self.sections_by_number is None: - coq_code, all_filenames = self.__get_coq_code() - spec = self.__process_lines(coq_code, all_filenames, self.spec_regex) + rocq_code, all_filenames = self.__get_rocq_code() + spec = self.__process_lines(rocq_code, all_filenames, self.spec_regex) self.sections_by_number = self.__get_comment_titles(spec) - directives = self.__process_lines(coq_code, all_filenames, self.directive_regex) + directives = self.__process_lines(rocq_code, all_filenames, self.directive_regex) for section in self.__parse_directives(directives): self.sections_by_number[section] = WildCard(None) return ParsedPage(self.name, Dictionary(None, self.sections_by_number)) diff --git a/tests/fuzzer/dune b/tests/fuzzer/dune index 74f9dc7..d5c22a7 100644 --- a/tests/fuzzer/dune +++ b/tests/fuzzer/dune @@ -16,7 +16,7 @@ (run npx webpack ./%{entrypoint} --config %{config} --no-stats) (copy dist/%{target} %{target}) (run chmod u+x %{target})))) - (enabled_if %{bin-available:webpack-cli})) + (enabled_if %{bin-available:webpack})) (rule (target warblre-node-fuzzer.js) @@ -24,7 +24,7 @@ (echo "Webpack-cli not installed: skipping fuzzer\n") (write-file %{target} "#!/usr/bin/env sh\necho \"Webpack-cli was not installed at build-time: cannot execute 'fuzzer', which was not built.\"\nexit 1") (run chmod u+x %{target}))) - (enabled_if (not %{bin-available:webpack-cli}))) + (enabled_if (not %{bin-available:webpack}))) (install (section bin) diff --git a/tests/test262/dune b/tests/test262/dune index 9d7918d..c7a6b9e 100644 --- a/tests/test262/dune +++ b/tests/test262/dune @@ -16,11 +16,11 @@ (run npx webpack ./%{entrypoint} --config %{config} --no-stats) (copy dist/warblre-node-redirect.js warblre-node-redirect.js) (copy dist/warblre-browser-redirect.js warblre-browser-redirect.js)))) - (enabled_if %{bin-available:webpack-cli})) + (enabled_if %{bin-available:webpack})) (rule (target dummy) (action (progn (echo "Webpack-cli not installed: skipping test262\n") (write-file dummy ""))) - (enabled_if (not %{bin-available:webpack-cli}))) \ No newline at end of file + (enabled_if (not %{bin-available:webpack}))) \ No newline at end of file diff --git a/warblre-engines.opam b/warblre-engines.opam index 2e18da2..fbabc41 100644 --- a/warblre-engines.opam +++ b/warblre-engines.opam @@ -7,7 +7,7 @@ license: "BSD-3-Clause" homepage: "https://github.com/epfl-systemf/warblre" bug-reports: "https://github.com/epfl-systemf/warblre/issues" depends: [ - "dune" {>= "3.14"} + "dune" {>= "3.21"} "warblre" {= version} "integers" {>= "0.7.0"} "uucp" {>= "15.0.0"} @@ -30,3 +30,4 @@ build: [ "@doc" {with-doc} ] ] +x-maintenance-intent: ["(latest)"] diff --git a/warblre.opam b/warblre.opam index 6f2be21..e983cda 100644 --- a/warblre.opam +++ b/warblre.opam @@ -7,9 +7,9 @@ license: "BSD-3-Clause" homepage: "https://github.com/epfl-systemf/warblre" bug-reports: "https://github.com/epfl-systemf/warblre/issues" depends: [ - "dune" {>= "3.14"} + "dune" {>= "3.21"} "ocaml" {= "4.14.2"} - "coq" {>= "8.18.0" & <= "8.19.2"} + "rocq-prover" {>= "9.0.0"} "odoc" {with-doc} ] build: [ @@ -26,3 +26,4 @@ build: [ "@doc" {with-doc} ] ] +x-maintenance-intent: ["(latest)"]