From 1b8a759c986f698ac5507c727a9259ed4ffa77dc Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 25 Nov 2025 18:53:13 +0100 Subject: [PATCH 01/23] Rocq9: rename in documentation --- README.md | 16 +++++------ doc/Differences.md | 13 +++++---- doc/Implementation.md | 65 ++++++++++++++++++++++++++----------------- etc/archi.svg | 12 ++++---- 4 files changed, 61 insertions(+), 45 deletions(-) diff --git a/README.md b/README.md index 971397d..783bd01 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,7 +26,7 @@ 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 @@ -55,7 +55,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. Alternatively, if you installed Alectryon, you can open the generated [webpage](_build/default/examples/rocq_proof/Example.html) in your web browser. ## Structure of the repository @@ -76,7 +76,7 @@ The repository is structured as follows: ├── examples │ ├── browser_playground │ ├── cmd_playground -│ ├── coq_proof +│ ├── rocq_proof │ └── ocaml_example └── tests ├── tests @@ -84,7 +84,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 +96,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 +115,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/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 Date: Tue, 25 Nov 2025 19:06:12 +0100 Subject: [PATCH 02/23] Rocq9: rename in specification_check --- specification_check/main.py | 10 +-- .../{coq_parser.py => rocq_parser.py} | 89 +++++++++---------- 2 files changed, 49 insertions(+), 50 deletions(-) rename specification_check/{coq_parser.py => rocq_parser.py} (84%) 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 84% rename from specification_check/coq_parser.py rename to specification_check/rocq_parser.py index 38955bd..8876614 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, coq_partition 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] + file = rocq_code[filename] partition = coq_partition(file) 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)) From d929c4e48d7f81ba840cf3f99682f1f5501e7ed2 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 25 Nov 2025 21:16:27 +0100 Subject: [PATCH 03/23] Rocq9: bump coq opam version --- .gitignore | 7 +++++-- dune-project | 2 +- engines/common/Extraction.v | 12 ++++++------ examples/{coq_proof => rocq_proof}/Example.v | 4 ++-- examples/{coq_proof => rocq_proof}/_CoqProject | 0 examples/{coq_proof => rocq_proof}/dune | 2 +- mechanization/props/Compile.v | 4 ++-- mechanization/props/Definitions.v | 2 +- mechanization/props/EarlyErrors.v | 2 +- mechanization/props/Match.v | 4 ++-- mechanization/props/NodeProps.v | 3 +-- mechanization/props/StrictlyNullable.v | 2 +- mechanization/spec/API.v | 2 +- mechanization/spec/Frontend.v | 2 +- mechanization/spec/Inst.v | 12 ++++++------ mechanization/spec/Node.v | 4 ++-- mechanization/spec/Notation.v | 2 +- mechanization/spec/Parameters.v | 8 ++++---- mechanization/spec/Patterns.v | 2 +- mechanization/spec/Semantics.v | 4 ++-- mechanization/spec/StaticSemantics.v | 2 +- mechanization/spec/base/Base.v | 4 ++-- mechanization/spec/base/Characters.v | 2 +- mechanization/spec/base/Coercions.v | 4 ++-- mechanization/spec/base/Numeric.v | 4 ++-- mechanization/tactics/Tactics.v | 8 ++++---- mechanization/utils/List.v | 4 ++-- mechanization/utils/Typeclasses.v | 2 +- warblre.opam | 2 +- 29 files changed, 57 insertions(+), 55 deletions(-) rename examples/{coq_proof => rocq_proof}/Example.v (98%) rename examples/{coq_proof => rocq_proof}/_CoqProject (100%) rename examples/{coq_proof => rocq_proof}/dune (83%) diff --git a/.gitignore b/.gitignore index 608e60e..e7f7dee 100644 --- a/.gitignore +++ b/.gitignore @@ -1,10 +1,13 @@ -# Coq(ide) generated files +# Rocq/CoqIDE generated files .lia.cache \#*\# # Dune's build directory _build/ +# Opam's directory +_opam/ + # VsCode's configuration .vscode/ @@ -16,4 +19,4 @@ _build/ node_modules # python -*/__pycache__ \ No newline at end of file +*/__pycache__ diff --git a/dune-project b/dune-project index 1e793ec..0fcdca4 100644 --- a/dune-project +++ b/dune-project @@ -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"))))) + (coq (>= 9.1.0)))) (package (name warblre-engines) diff --git a/engines/common/Extraction.v b/engines/common/Extraction.v index 6b6b69f..ce96cc0 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,13 @@ *) 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. -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" ] @@ -89,4 +89,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/examples/coq_proof/Example.v b/examples/rocq_proof/Example.v similarity index 98% rename from examples/coq_proof/Example.v rename to examples/rocq_proof/Example.v index bda7dc6..9c9f8ac 100644 --- a/examples/coq_proof/Example.v +++ b/examples/rocq_proof/Example.v @@ -1,4 +1,4 @@ -From Coq Require Import ZArith List. +From Stdlib Require Import ZArith List. From Warblre Require Import Parameters. From Warblre Require Import Patterns RegExpRecord. From Warblre Require Import EarlyErrors. @@ -10,7 +10,7 @@ Import Patterns Coercions.Coercions Notation.Notation. (** This file demonstrates how our specification can be used to reason about regular expressions. - Specifically, we prove an extremely simple property: the fact that for any [a], the regexp [/(?:a+?)+?/] matches the string ["aaa"] (the paper describes more complex proofs, and the global README links to the corresponding Coq code). **) + Specifically, we prove an extremely simple property: the fact that for any [a], the regexp [/(?:a+?)+?/] matches the string ["aaa"] (the paper describes more complex proofs, and the global README links to the corresponding Rocq code). **) Section AbstractMatching. (** We start by assuming a concrete (yet arbitrary) instantiation of the engine. **) diff --git a/examples/coq_proof/_CoqProject b/examples/rocq_proof/_CoqProject similarity index 100% rename from examples/coq_proof/_CoqProject rename to examples/rocq_proof/_CoqProject diff --git a/examples/coq_proof/dune b/examples/rocq_proof/dune similarity index 83% rename from examples/coq_proof/dune rename to examples/rocq_proof/dune index 7d67997..b32ad21 100644 --- a/examples/coq_proof/dune +++ b/examples/rocq_proof/dune @@ -8,6 +8,6 @@ (rule (target dummy) (action (progn - (echo "Alectryon not installed: skipping examples/coq_proof\n") + (echo "Alectryon not installed: skipping examples/rocq_proof\n") (write-file dummy ""))) (enabled_if (not %{bin-available:alectryon}))) \ No newline at end of file diff --git a/mechanization/props/Compile.v b/mechanization/props/Compile.v index 7ec71c7..520ccfd 100644 --- a/mechanization/props/Compile.v +++ b/mechanization/props/Compile.v @@ -1,4 +1,4 @@ -From Coq Require Import PeanoNat ZArith Bool Lia Program.Equality List. +From Stdlib Require Import PeanoNat ZArith Bool Lia Program.Equality List. From Warblre Require Import List Tactics Specialize Focus Result Base Errors Patterns Node NodeProps StaticSemantics Notation Semantics Definitions EarlyErrors RegExpRecord. Import Result.Notations. @@ -163,4 +163,4 @@ Section Compile. - exists s. reflexivity. - pose proof (compilePattern r rer) as Falsum. fforward Falsum. contradiction. Qed. -End Compile. \ No newline at end of file +End Compile. diff --git a/mechanization/props/Definitions.v b/mechanization/props/Definitions.v index 5e11401..620c410 100644 --- a/mechanization/props/Definitions.v +++ b/mechanization/props/Definitions.v @@ -1,4 +1,4 @@ -From Coq Require Import Bool ZArith. +From Stdlib Require Import Bool ZArith. From Warblre Require Import Tactics Specialize Focus Result Base Errors Patterns Node StaticSemantics Notation Semantics Coercions. Import Result.Notations. Local Open Scope result_flow. diff --git a/mechanization/props/EarlyErrors.v b/mechanization/props/EarlyErrors.v index 2c1c59b..05d58e7 100644 --- a/mechanization/props/EarlyErrors.v +++ b/mechanization/props/EarlyErrors.v @@ -1,4 +1,4 @@ -From Coq Require Import PeanoNat List Lia NArith Program.Equality. +From Stdlib Require Import PeanoNat List Lia NArith Program.Equality. From Warblre Require Import Tactics List Result Errors Focus Base Characters Patterns Node NodeProps StaticSemantics. Section EarlyErrors. diff --git a/mechanization/props/Match.v b/mechanization/props/Match.v index 68b3cfb..5fa416c 100644 --- a/mechanization/props/Match.v +++ b/mechanization/props/Match.v @@ -1,4 +1,4 @@ -From Coq Require Import PeanoNat ZArith Bool Lia Program.Equality List. +From Stdlib Require Import PeanoNat ZArith Bool Lia Program.Equality List. From Warblre Require Import List Tactics Retrieve Specialize Focus Result Base Errors Patterns Node NodeProps StaticSemantics Notation Semantics Definitions EarlyErrors Compile RegExpRecord. Import Result.Notations. @@ -1030,4 +1030,4 @@ Module Match. + (* Success => 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/Frontend.v b/mechanization/spec/Frontend.v index d15aef4..0482061 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. diff --git a/mechanization/spec/Inst.v b/mechanization/spec/Inst.v index 4b0aaa7..e65080a 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. @@ -534,10 +534,10 @@ Definition get_success {S F} (r: Result S F) : match r with Success _ => S | Err | 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 := 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..e0a8c7f 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,7 +356,7 @@ 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. *) +(* Used in Frontend.v due to bug in Rocq 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. *) @@ -377,4 +377,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/Tactics.v b/mechanization/tactics/Tactics.v index ea98cc2..ee5f26a 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 + Stdlib.Program.Tactics.destruct_conjs + || Stdlib.Program.Tactics.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..11639e5 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. @@ -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..d33e6b7 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. diff --git a/warblre.opam b/warblre.opam index 6f2be21..bab01aa 100644 --- a/warblre.opam +++ b/warblre.opam @@ -9,7 +9,7 @@ bug-reports: "https://github.com/epfl-systemf/warblre/issues" depends: [ "dune" {>= "3.14"} "ocaml" {= "4.14.2"} - "coq" {>= "8.18.0" & <= "8.19.2"} + "coq" {>= "9.1.0"} "odoc" {with-doc} ] build: [ From e3f82c2b5a3b384b316d18a921acb061ca9a07ae Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 25 Nov 2025 21:20:43 +0100 Subject: [PATCH 04/23] Rocq9: bump version in CI --- .github/workflows/ci.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4cf0e04..6bdb81a 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" ] + rocq: [ "9.1.0" ] node: [ "21.7.2", "22.4.1" ] 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,7 +62,7 @@ jobs: echo "::endgroup::" echo "::group::Install opam packages" - opam pin add -n -k version coq ${{ matrix.coq }} + opam pin add -n -k version coq ${{ matrix.rocq }} # 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 From c3f4dde7aac56b451faff56962eb0091e3d8bbae Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 25 Nov 2025 21:44:54 +0100 Subject: [PATCH 05/23] Rocq9: disable SerAPI temporarily --- .github/workflows/ci.yml | 4 ++-- dune-project | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6bdb81a..876d698 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -63,9 +63,9 @@ jobs: echo "::group::Install opam packages" opam pin add -n -k version coq ${{ matrix.rocq }} + opam install --confirm-level=unsafe-yes --deps-only . # 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 install --confirm-level=unsafe-yes coq-serapi echo "::endgroup::" echo "::group::Print opam config (post-install)" diff --git a/dune-project b/dune-project index 0fcdca4..7dd9418 100644 --- a/dune-project +++ b/dune-project @@ -19,6 +19,7 @@ (synopsis "A mechanization of the specification of ECMAScript regexes") (depends (ocaml (= 4.14.2)) + ; LATER: move to rocq-prover once dune plugin is updated: https://github.com/ocaml/dune/pull/12035 (coq (>= 9.1.0)))) (package From 634f53bc136e4b10a080e48547b3769899465786 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 25 Nov 2025 23:12:53 +0100 Subject: [PATCH 06/23] Rocq9: add Stdlib to theories and fix deprecations --- engines/js/dune | 2 +- engines/ocaml/dune | 4 ++-- mechanization/dune | 2 +- mechanization/spec/Inst.v | 6 +++--- mechanization/tactics/Tactics.v | 4 ++-- mechanization/utils/List.v | 2 +- 6 files changed, 10 insertions(+), 10 deletions(-) diff --git a/engines/js/dune b/engines/js/dune index b6bff71..a3f447f 100644 --- a/engines/js/dune +++ b/engines/js/dune @@ -10,7 +10,7 @@ (coq.extraction (prelude Extraction) (extracted_modules Extracted) - (theories Warblre Ltac2)) + (theories Warblre Ltac2 Stdlib)) ; Make a library out of it (library diff --git a/engines/ocaml/dune b/engines/ocaml/dune index 46b3186..be3f817 100644 --- a/engines/ocaml/dune +++ b/engines/ocaml/dune @@ -10,7 +10,7 @@ (coq.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/mechanization/dune b/mechanization/dune index a960512..a6c5e45 100644 --- a/mechanization/dune +++ b/mechanization/dune @@ -3,4 +3,4 @@ (coq.theory (name Warblre) (package warblre) - (theories Ltac2)) + (theories Ltac2 Stdlib)) diff --git a/mechanization/spec/Inst.v b/mechanization/spec/Inst.v index e65080a..9c83448 100644 --- a/mechanization/spec/Inst.v +++ b/mechanization/spec/Inst.v @@ -528,7 +528,7 @@ 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 @@ -548,8 +548,8 @@ 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 diff --git a/mechanization/tactics/Tactics.v b/mechanization/tactics/Tactics.v index ee5f26a..01e5720 100644 --- a/mechanization/tactics/Tactics.v +++ b/mechanization/tactics/Tactics.v @@ -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 ( - Stdlib.Program.Tactics.destruct_conjs - || Stdlib.Program.Tactics.clear_dups + destruct_conjs + || clear_dups || subst || lazymatch goal with | [ H: _ = _ |- _ ] => clean_injection H || discriminate H diff --git a/mechanization/utils/List.v b/mechanization/utils/List.v index 11639e5..62eb0d5 100644 --- a/mechanization/utils/List.v +++ b/mechanization/utils/List.v @@ -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. From 1ff1c801b7717799145fc2b64ee306439dcb1b42 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Tue, 25 Nov 2025 23:36:19 +0100 Subject: [PATCH 07/23] Rocq9: fix some old LATERs --- mechanization/spec/Errors.v | 8 +++----- mechanization/spec/Frontend.v | 7 ++----- mechanization/spec/Parameters.v | 3 --- mechanization/tactics/Retrieve.v | 9 +-------- mechanization/utils/Typeclasses.v | 5 ++--- 5 files changed, 8 insertions(+), 24 deletions(-) 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 0482061..e892299 100644 --- a/mechanization/spec/Frontend.v +++ b/mechanization/spec/Frontend.v @@ -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/Parameters.v b/mechanization/spec/Parameters.v index e0a8c7f..0edad35 100644 --- a/mechanization/spec/Parameters.v +++ b/mechanization/spec/Parameters.v @@ -356,9 +356,6 @@ Module Parameters. End Parameters. Notation Parameters := @Parameters.class. -(* Used in Frontend.v due to bug in Rocq 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}. 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/utils/Typeclasses.v b/mechanization/utils/Typeclasses.v index d33e6b7..1726a01 100644 --- a/mechanization/utils/Typeclasses.v +++ b/mechanization/utils/Typeclasses.v @@ -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. From 5affa13fd7e686e4864265dfbc9f910d61a7b736 Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Tue, 25 Nov 2025 22:00:30 -0500 Subject: [PATCH 08/23] Update flake to Rocq (9.1) --- flake.lock | 99 ++++++++---------------------------------------------- flake.nix | 26 ++++++-------- 2 files changed, 24 insertions(+), 101 deletions(-) diff --git a/flake.lock b/flake.lock index 4aeeec1..d7ffd2f 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1710146030, - "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", "owner": "numtide", "repo": "flake-utils", - "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", "type": "github" }, "original": { @@ -18,101 +18,34 @@ "type": "github" } }, - "melange": { - "inputs": { - "flake-utils": [ - "flake-utils" - ], - "melange-compiler-libs": "melange-compiler-libs", - "nix-filter": "nix-filter", - "nixpkgs": [ - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1707255164, - "narHash": "sha256-eJ2+nbjEGnTinf67lhUPuE8fzfGXeC2ErGRvU2omUgs=", - "owner": "melange-re", - "repo": "melange", - "rev": "71cc9a89b4236cbf02668b21602e86b653b9a6a0", - "type": "github" - }, - "original": { - "owner": "melange-re", - "ref": "v3-414", - "repo": "melange", - "type": "github" - } - }, - "melange-compiler-libs": { - "inputs": { - "flake-utils": [ - "melange", - "flake-utils" - ], - "nixpkgs": [ - "melange", - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1705107784, - "narHash": "sha256-tN+g+m2yXUL5Mik2I0SbMDhhoqatHL/it0VR9cjVYag=", - "owner": "melange-re", - "repo": "melange-compiler-libs", - "rev": "2c06d6ea9257c52a18cef82f154307eaa2a1bbae", - "type": "github" - }, - "original": { - "owner": "melange-re", - "ref": "4.14", - "repo": "melange-compiler-libs", - "type": "github" - } - }, - "nix-filter": { - "locked": { - "lastModified": 1705332318, - "narHash": "sha256-kcw1yFeJe9N4PjQji9ZeX47jg0p9A0DuU4djKvg1a7I=", - "owner": "numtide", - "repo": "nix-filter", - "rev": "3449dc925982ad46246cfc36469baf66e1b64f17", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "nix-filter", - "type": "github" - } - }, "nixpkgs": { "locked": { - "lastModified": 1713995372, - "narHash": "sha256-fFE3M0vCoiSwCX02z8VF58jXFRj9enYUSTqjyHAjrds=", - "owner": "NixOS", + "lastModified": 1763966396, + "narHash": "sha256-6eeL1YPcY1MV3DDStIDIdy/zZCDKgHdkCmsrLJFiZf0=", + "owner": "nixos", "repo": "nixpkgs", - "rev": "dd37924974b9202f8226ed5d74a252a9785aedf8", + "rev": "5ae3b07d8d6527c42f17c876e404993199144b6a", "type": "github" }, "original": { "owner": "nixos", - "ref": "nixos-23.11", + "ref": "nixos-unstable", "repo": "nixpkgs", "type": "github" } }, - "nixpkgs-unstable": { + "nixpkgs_2": { "locked": { - "lastModified": 1716509168, - "narHash": "sha256-4zSIhSRRIoEBwjbPm3YiGtbd8HDWzFxJjw5DYSDy1n8=", + "lastModified": 1720535198, + "narHash": "sha256-zwVvxrdIzralnSbcpghA92tWu2DV2lwv89xZc8MTrbg=", "owner": "nixos", "repo": "nixpkgs", - "rev": "bfb7a882678e518398ce9a31a881538679f6f092", + "rev": "205fd4226592cc83fd4c0885a3e4c9c400efabb5", "type": "github" }, "original": { "owner": "nixos", - "ref": "nixos-unstable", + "ref": "nixos-23.11", "repo": "nixpkgs", "type": "github" } @@ -120,9 +53,7 @@ "root": { "inputs": { "flake-utils": "flake-utils", - "melange": "melange", "nixpkgs": "nixpkgs", - "nixpkgs-unstable": "nixpkgs-unstable", "spec-merger": "spec-merger" } }, @@ -131,9 +62,7 @@ "flake-utils": [ "flake-utils" ], - "nixpkgs": [ - "nixpkgs" - ] + "nixpkgs": "nixpkgs_2" }, "locked": { "dir": ".nix", diff --git a/flake.nix b/flake.nix index c9e7652..05e12ed 100644 --- a/flake.nix +++ b/flake.nix @@ -2,26 +2,19 @@ description = "A mechanization of the specification of ECMAScript regexes."; inputs = { - nixpkgs.url = "github:nixos/nixpkgs/nixos-23.11"; - nixpkgs-unstable.url = "github:nixos/nixpkgs/nixos-unstable"; + nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-utils.url = "github:numtide/flake-utils"; spec-merger = { url = "github:Ef55/SpecMerger/38ac474cca1788ec4fb4d85ecaaa8c81aecf41f6?dir=.nix"; - inputs.nixpkgs.follows = "nixpkgs"; - inputs.flake-utils.follows = "flake-utils"; - }; - melange = { - url = "github:melange-re/melange/v3-414"; - inputs.nixpkgs.follows = "nixpkgs"; + # inputs.nixpkgs.follows = "nixpkgs"; inputs.flake-utils.follows = "flake-utils"; }; }; - outputs = { self, nixpkgs, nixpkgs-unstable, spec-merger, flake-utils, melange }@input: + outputs = { self, nixpkgs, spec-merger, flake-utils }@input: flake-utils.lib.eachDefaultSystem (system: let - pkgs = import nixpkgs { inherit system; overlays = [ melange.overlays.default ]; }; - pkgs-unstable = import nixpkgs-unstable { inherit system; }; + pkgs = nixpkgs.legacyPackages.${system}; spec-diff = pkgs.writeShellApplication { name = "spec-diff"; @@ -37,10 +30,11 @@ devShells = { default = pkgs.mkShell { buildInputs = with pkgs; [ - coq + coq_9_1 + coqPackages_9_1.stdlib ocaml - pkgs-unstable.dune_3 + dune_3 ocamlPackages.ocamlformat ocamlPackages.ocaml-lsp ocamlPackages.findlib @@ -50,12 +44,12 @@ ocamlPackages.melange ocamlPackages.zarith - coqPackages.serapi - python311Packages.alectryon + # coqPackages.serapi + # python311Packages.alectryon spec-merger.packages.${system}.spec-merger spec-diff - nodejs_21 + nodejs_24 nodePackages.webpack-cli ]; }; From 501210c577f3bb2116eefeb70a4ebd6ba77a90f6 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Fri, 28 Nov 2025 13:38:49 +0100 Subject: [PATCH 09/23] WIP: use dune's new rocq plugin --- dune-project | 7 +++---- engines/js/dune | 2 +- engines/ocaml/dune | 2 +- examples/rocq_proof/_CoqProject | 1 - mechanization/_CoqProject | 1 - mechanization/dune | 2 +- warblre-engines.opam | 3 ++- warblre.opam | 5 +++-- 8 files changed, 11 insertions(+), 12 deletions(-) delete mode 100644 examples/rocq_proof/_CoqProject delete mode 100644 mechanization/_CoqProject diff --git a/dune-project b/dune-project index 7dd9418..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,8 +19,7 @@ (synopsis "A mechanization of the specification of ECMAScript regexes") (depends (ocaml (= 4.14.2)) - ; LATER: move to rocq-prover once dune plugin is updated: https://github.com/ocaml/dune/pull/12035 - (coq (>= 9.1.0)))) + (rocq-prover (>= 9.0.0)))) (package (name warblre-engines) diff --git a/engines/js/dune b/engines/js/dune index a3f447f..7ac58f5 100644 --- a/engines/js/dune +++ b/engines/js/dune @@ -7,7 +7,7 @@ (files ../common/Extraction.v)) ; Extract with different directives -(coq.extraction +(rocq.extraction (prelude Extraction) (extracted_modules Extracted) (theories Warblre Ltac2 Stdlib)) diff --git a/engines/ocaml/dune b/engines/ocaml/dune index be3f817..46660fe 100644 --- a/engines/ocaml/dune +++ b/engines/ocaml/dune @@ -7,7 +7,7 @@ (files ../common/Extraction.v)) ; Extract with different directives -(coq.extraction +(rocq.extraction (prelude Extraction) (extracted_modules Extracted) (theories Warblre Ltac2 Stdlib)) diff --git a/examples/rocq_proof/_CoqProject b/examples/rocq_proof/_CoqProject deleted file mode 100644 index 0bce3e0..0000000 --- a/examples/rocq_proof/_CoqProject +++ /dev/null @@ -1 +0,0 @@ --Q ../../_build/default/mechanization Warblre \ No newline at end of file diff --git a/mechanization/_CoqProject b/mechanization/_CoqProject deleted file mode 100644 index 85caf5d..0000000 --- a/mechanization/_CoqProject +++ /dev/null @@ -1 +0,0 @@ --Q ../_build/default/mechanization Warblre \ No newline at end of file diff --git a/mechanization/dune b/mechanization/dune index a6c5e45..3cf92c5 100644 --- a/mechanization/dune +++ b/mechanization/dune @@ -1,6 +1,6 @@ (include_subdirs qualified) -(coq.theory +(rocq.theory (name Warblre) (package warblre) (theories Ltac2 Stdlib)) 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 bab01aa..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" {>= "9.1.0"} + "rocq-prover" {>= "9.0.0"} "odoc" {with-doc} ] build: [ @@ -26,3 +26,4 @@ build: [ "@doc" {with-doc} ] ] +x-maintenance-intent: ["(latest)"] From 9da2c9286f39e1b58dcd8e340a3cb054b066c0e4 Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Tue, 2 Dec 2025 22:00:42 -0500 Subject: [PATCH 10/23] Update dune/rocq to bleeding-edge in nix flake; fix warnings --- .nix/dune.nix | 57 ++++++++++++++++++++++++++++ .nix/vsrocq-language-server.nix | 64 ++++++++++++++++++++++++++++++++ engines/common/Extraction.v | 1 + engines/js/dune | 2 +- examples/browser_playground/dune | 4 +- examples/cmd_playground/dune | 4 +- flake.lock | 6 +-- flake.nix | 30 ++++++++------- mechanization/tactics/Focus.v | 29 ++++++++------- package-lock.json | 7 +++- tests/fuzzer/dune | 4 +- tests/test262/dune | 4 +- 12 files changed, 172 insertions(+), 40 deletions(-) create mode 100644 .nix/dune.nix create mode 100644 .nix/vsrocq-language-server.nix 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..80f602d --- /dev/null +++ b/.nix/vsrocq-language-server.nix @@ -0,0 +1,64 @@ +# 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 + yojson + zarith + ppx_inline_test + ppx_assert + ppx_sexp_conv + ppx_deriving + ppx_import + sexplib + ppx_yojson_conv + 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/engines/common/Extraction.v b/engines/common/Extraction.v index ce96cc0..89c3766 100644 --- a/engines/common/Extraction.v +++ b/engines/common/Extraction.v @@ -13,6 +13,7 @@ From Stdlib Require Import ZArith. From Stdlib Require Extraction. Extraction Language OCaml. +Set Extraction Output Directory ".". From Stdlib Require extraction.ExtrOcamlBasic. From Stdlib Require extraction.ExtrOcamlString. diff --git a/engines/js/dune b/engines/js/dune index 7ac58f5..4622525 100644 --- a/engines/js/dune +++ b/engines/js/dune @@ -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/examples/browser_playground/dune b/examples/browser_playground/dune index 557eab3..a3bb054 100644 --- a/examples/browser_playground/dune +++ b/examples/browser_playground/dune @@ -15,11 +15,11 @@ (action (no-infer (progn (run npx webpack ./%{entrypoint} --config %{config} --no-stats) (copy dist/%{target} %{target})))) - (enabled_if %{bin-available:webpack-cli})) + (enabled_if %{bin-available:webpack})) (rule (target dummy) (action (progn (echo "Webpack-cli not installed: skipping examples/browser_playground\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/examples/cmd_playground/dune b/examples/cmd_playground/dune index 305c2cb..034685a 100644 --- a/examples/cmd_playground/dune +++ b/examples/cmd_playground/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})) ; This way of handling missing JS dependencies is dirty, but it's the best I managed (rule @@ -25,7 +25,7 @@ (echo "Webpack-cli not installed: skipping cmd_playground\n") (write-file %{target} "#!/usr/bin/env sh\necho \"Webpack-cli was not installed at build-time: cannot execute 'playground', 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/flake.lock b/flake.lock index d7ffd2f..2245e5a 100644 --- a/flake.lock +++ b/flake.lock @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1763966396, - "narHash": "sha256-6eeL1YPcY1MV3DDStIDIdy/zZCDKgHdkCmsrLJFiZf0=", + "lastModified": 1764242076, + "narHash": "sha256-sKoIWfnijJ0+9e4wRvIgm/HgE27bzwQxcEmo2J/gNpI=", "owner": "nixos", "repo": "nixpkgs", - "rev": "5ae3b07d8d6527c42f17c876e404993199144b6a", + "rev": "2fad6eac6077f03fe109c4d4eb171cf96791faa4", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 05e12ed..cf13f6f 100644 --- a/flake.nix +++ b/flake.nix @@ -16,6 +16,8 @@ let pkgs = nixpkgs.legacyPackages.${system}; + oPkgs = pkgs.ocaml-ng.ocamlPackages_4_14; + spec-diff = pkgs.writeShellApplication { name = "spec-diff"; runtimeInputs = with pkgs; [ @@ -30,19 +32,21 @@ devShells = { default = pkgs.mkShell { buildInputs = with pkgs; [ - coq_9_1 - coqPackages_9_1.stdlib - - ocaml - dune_3 - ocamlPackages.ocamlformat - ocamlPackages.ocaml-lsp - ocamlPackages.findlib - ocamlPackages.integers - ocamlPackages.uucp - ocamlPackages.ppx_expect - ocamlPackages.melange - ocamlPackages.zarith + rocqPackages_9_1.rocq-core + rocqPackages_9_1.stdlib + (rocqPackages_9_1.callPackage .nix/vsrocq-language-server.nix {}) + + # TODO: switch back to the packages in nixpkgs once the features we need get released + oPkgs.ocaml + (oPkgs.callPackage .nix/dune.nix {}) + oPkgs.ocamlformat + oPkgs.ocaml-lsp + oPkgs.findlib + oPkgs.integers + oPkgs.uucp + oPkgs.ppx_expect + oPkgs.melange + oPkgs.zarith # coqPackages.serapi # python311Packages.alectryon 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/package-lock.json b/package-lock.json index 21d32fa..16da5b4 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,5 +1,5 @@ { - "name": "warblre", + "name": "Warblre", "lockfileVersion": 3, "requires": true, "packages": { @@ -315,6 +315,7 @@ "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.12.1.tgz", "integrity": "sha512-tcpGyI9zbizT9JbV6oYE477V6mTlXvvi0T0G3SNIYE2apm/G5huBa1+K89VGeovbg+jycCrfhl3ADxErOuO6Jg==", "dev": true, + "peer": true, "bin": { "acorn": "bin/acorn" }, @@ -336,6 +337,7 @@ "resolved": "https://registry.npmjs.org/ajv/-/ajv-6.12.6.tgz", "integrity": "sha512-j3fVLgvTo527anyYyJOGTYJbG+vnnQYvE0m5mmkc1TK+nxAppkCLMIL0aZ4dblVCNoGShhm+kzE4ZUykBoMg4g==", "dev": true, + "peer": true, "dependencies": { "fast-deep-equal": "^3.1.1", "fast-json-stable-stringify": "^2.0.0", @@ -375,6 +377,7 @@ "url": "https://github.com/sponsors/ai" } ], + "peer": true, "dependencies": { "caniuse-lite": "^1.0.30001663", "electron-to-chromium": "^1.5.28", @@ -1207,6 +1210,7 @@ "resolved": "https://registry.npmjs.org/webpack/-/webpack-5.95.0.tgz", "integrity": "sha512-2t3XstrKULz41MNMBF+cJ97TyHdyQ8HCt//pqErqDvNjU9YQBnZxIHa11VXsi7F3mb5/aO2tuDxdeTPdU7xu9Q==", "dev": true, + "peer": true, "dependencies": { "@types/estree": "^1.0.5", "@webassemblyjs/ast": "^1.12.1", @@ -1253,6 +1257,7 @@ "resolved": "https://registry.npmjs.org/webpack-cli/-/webpack-cli-5.1.4.tgz", "integrity": "sha512-pIDJHIEI9LR0yxHXQ+Qh95k2EvXpWzZ5l+d+jIo+RdSm9MiHfzazIxwwni/p7+x4eJZuvG1AJwgC4TNQ7NRgsg==", "dev": true, + "peer": true, "dependencies": { "@discoveryjs/json-ext": "^0.5.0", "@webpack-cli/configtest": "^2.1.1", 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 From e37e13b966a4a235d0a0fc814c2fd8e8992a7558 Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Tue, 2 Dec 2025 22:09:17 -0500 Subject: [PATCH 11/23] Generate `_RocqProject` using dune --- .gitignore | 3 +++ mechanization/dune | 1 + 2 files changed, 4 insertions(+) diff --git a/.gitignore b/.gitignore index e7f7dee..fe25899 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,9 @@ .lia.cache \#*\# +# This file gets generated by dune, and contains install-dependent paths +_RocqProject + # Dune's build directory _build/ diff --git a/mechanization/dune b/mechanization/dune index 3cf92c5..561dd47 100644 --- a/mechanization/dune +++ b/mechanization/dune @@ -3,4 +3,5 @@ (rocq.theory (name Warblre) (package warblre) + (generate_project_file) (theories Ltac2 Stdlib)) From 698dbdc30ea6cca708a9bfee7ae664a974988113 Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Thu, 4 Dec 2025 19:35:13 -0500 Subject: [PATCH 12/23] Update npm packages --- package-lock.json | 736 ++++++++++++++++++++++++++++------------------ 1 file changed, 455 insertions(+), 281 deletions(-) diff --git a/package-lock.json b/package-lock.json index 16da5b4..2b8ee4d 100644 --- a/package-lock.json +++ b/package-lock.json @@ -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,22 @@ "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" @@ -323,45 +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": [ { @@ -377,12 +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" @@ -395,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": [ { @@ -415,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" } @@ -431,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", @@ -444,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", @@ -467,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" @@ -486,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" }, @@ -498,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" } @@ -517,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" @@ -530,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" }, @@ -542,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" } @@ -551,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" } @@ -560,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" } @@ -568,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" } @@ -590,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" @@ -603,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" } @@ -612,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" } @@ -620,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" } @@ -642,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" }, @@ -654,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" @@ -673,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" }, @@ -697,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" }, @@ -708,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" } @@ -724,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", @@ -737,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": { @@ -768,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" }, @@ -779,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" } @@ -795,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" }, @@ -806,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" }, @@ -834,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" }, @@ -846,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" } @@ -855,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" } @@ -864,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" } @@ -872,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" }, @@ -892,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" } @@ -915,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" }, @@ -922,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" } @@ -944,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" }, @@ -956,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" } @@ -978,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" @@ -1003,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" } @@ -1012,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" }, @@ -1024,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" }, @@ -1036,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" } @@ -1045,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" } @@ -1054,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" @@ -1064,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" }, @@ -1079,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" }, @@ -1087,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" }, @@ -1114,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" @@ -1148,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": [ { @@ -1172,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" @@ -1183,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" @@ -1206,35 +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" @@ -1257,7 +1426,7 @@ "resolved": "https://registry.npmjs.org/webpack-cli/-/webpack-cli-5.1.4.tgz", "integrity": "sha512-pIDJHIEI9LR0yxHXQ+Qh95k2EvXpWzZ5l+d+jIo+RdSm9MiHfzazIxwwni/p7+x4eJZuvG1AJwgC4TNQ7NRgsg==", "dev": true, - "peer": true, + "license": "MIT", "dependencies": { "@discoveryjs/json-ext": "^0.5.0", "@webpack-cli/configtest": "^2.1.1", @@ -1303,6 +1472,7 @@ "resolved": "https://registry.npmjs.org/commander/-/commander-10.0.1.tgz", "integrity": "sha512-y4Mg2tXshplEbSGzx7amzPwKKOCGuoSRP/CjEdwwk0FOGlUbq6lKuoyDZTNZkmxHdJtp54hdfY/JUrdL7Xfdug==", "dev": true, + "license": "MIT", "engines": { "node": ">=14" } @@ -1312,6 +1482,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", @@ -1322,10 +1493,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" } @@ -1335,6 +1507,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" }, @@ -1349,7 +1522,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" } } } From b4b3fc789a0644b102ec46fe91763accb557452b Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Thu, 4 Dec 2025 19:38:44 -0500 Subject: [PATCH 13/23] Update SpecMerger in flake --- flake.lock | 31 ++++++++----------------------- flake.nix | 4 ++-- 2 files changed, 10 insertions(+), 25 deletions(-) diff --git a/flake.lock b/flake.lock index 2245e5a..b08b7ef 100644 --- a/flake.lock +++ b/flake.lock @@ -34,22 +34,6 @@ "type": "github" } }, - "nixpkgs_2": { - "locked": { - "lastModified": 1720535198, - "narHash": "sha256-zwVvxrdIzralnSbcpghA92tWu2DV2lwv89xZc8MTrbg=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "205fd4226592cc83fd4c0885a3e4c9c400efabb5", - "type": "github" - }, - "original": { - "owner": "nixos", - "ref": "nixos-23.11", - "repo": "nixpkgs", - "type": "github" - } - }, "root": { "inputs": { "flake-utils": "flake-utils", @@ -62,22 +46,23 @@ "flake-utils": [ "flake-utils" ], - "nixpkgs": "nixpkgs_2" + "nixpkgs": [ + "nixpkgs" + ] }, "locked": { "dir": ".nix", - "lastModified": 1744998158, - "narHash": "sha256-INH13MG/ty45xl7ppg6d3AelIZMPX34pTX7SjjsbBIE=", - "owner": "Ef55", + "lastModified": 1764761065, + "narHash": "sha256-XqZCU3Mjc+Zsm1pLvd4WTmYjqWRY11ghQ2QDSP7paXw=", + "owner": "epfl-systemf", "repo": "SpecMerger", - "rev": "38ac474cca1788ec4fb4d85ecaaa8c81aecf41f6", + "rev": "48a1342eb1e6078c74b56a900a44e050fc7f41b0", "type": "github" }, "original": { "dir": ".nix", - "owner": "Ef55", + "owner": "epfl-systemf", "repo": "SpecMerger", - "rev": "38ac474cca1788ec4fb4d85ecaaa8c81aecf41f6", "type": "github" } }, diff --git a/flake.nix b/flake.nix index cf13f6f..9d6daf2 100644 --- a/flake.nix +++ b/flake.nix @@ -5,8 +5,8 @@ nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-utils.url = "github:numtide/flake-utils"; spec-merger = { - url = "github:Ef55/SpecMerger/38ac474cca1788ec4fb4d85ecaaa8c81aecf41f6?dir=.nix"; - # inputs.nixpkgs.follows = "nixpkgs"; + url = "github:epfl-systemf/SpecMerger/?dir=.nix"; + inputs.nixpkgs.follows = "nixpkgs"; inputs.flake-utils.follows = "flake-utils"; }; }; From d57b8444b61c18d1bbbce41b772192d79db1b1c6 Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Thu, 4 Dec 2025 21:11:42 -0500 Subject: [PATCH 14/23] Rocq9: fix `Pos` extraction --- engines/common/Extraction.v | 38 ++++++++++++++++++++++++++----------- 1 file changed, 27 insertions(+), 11 deletions(-) diff --git a/engines/common/Extraction.v b/engines/common/Extraction.v index 89c3766..b1b8f1c 100644 --- a/engines/common/Extraction.v +++ b/engines/common/Extraction.v @@ -40,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 => From 30f984d0e401a5c578c1548466a01aa8c84fb546 Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Thu, 4 Dec 2025 21:13:52 -0500 Subject: [PATCH 15/23] Bump python's `request` version --- .github/pip-requirements.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/pip-requirements.txt b/.github/pip-requirements.txt index 153043b..19d92e4 100644 --- a/.github/pip-requirements.txt +++ b/.github/pip-requirements.txt @@ -1,4 +1,4 @@ alectryon == 1.4.0 git+https://github.com/epfl-systemf/SpecMerger -requests == 2.32.3 +requests == 2.32.4 beautifulsoup4 == 4.12.3 From a6606bcfda7b401686197de362e70a2b769e219c Mon Sep 17 00:00:00 2001 From: shilangyu Date: Sat, 17 Jan 2026 19:14:08 +0100 Subject: [PATCH 16/23] Disable alectryon for now --- .github/workflows/ci.yml | 2 -- README.md | 9 +-------- examples/rocq_proof/dune | 25 +++++++++++++------------ 3 files changed, 14 insertions(+), 22 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 876d698..13733eb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -64,8 +64,6 @@ jobs: echo "::group::Install opam packages" opam pin add -n -k version coq ${{ matrix.rocq }} opam install --confirm-level=unsafe-yes --deps-only . - # coq-serapi's dependencies are installed now to ensure - # opam install --confirm-level=unsafe-yes coq-serapi echo "::endgroup::" echo "::group::Print opam config (post-install)" diff --git a/README.md b/README.md index 783bd01..d37b38d 100644 --- a/README.md +++ b/README.md @@ -37,13 +37,6 @@ The mechanization has the following properties: 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: ``` nix develop @@ -55,7 +48,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/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. Alternatively, if you installed Alectryon, you can open the generated [webpage](_build/default/examples/rocq_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 diff --git a/examples/rocq_proof/dune b/examples/rocq_proof/dune index b32ad21..adb2424 100644 --- a/examples/rocq_proof/dune +++ b/examples/rocq_proof/dune @@ -1,13 +1,14 @@ -(rule - (target Example.html) - (deps (package warblre) (:input (file Example.v))) - (action - (run alectryon -Q ../../mechanization Warblre --long-line-threshold -1 %{input})) - (enabled_if %{bin-available:alectryon})) +; LATER: re-enable when Alectryon supports Coq 9.0 +; (rule +; (target Example.html) +; (deps (package warblre) (:input (file Example.v))) +; (action +; (run alectryon -Q ../../mechanization Warblre --long-line-threshold -1 %{input})) +; (enabled_if %{bin-available:alectryon})) -(rule - (target dummy) - (action (progn - (echo "Alectryon not installed: skipping examples/rocq_proof\n") - (write-file dummy ""))) - (enabled_if (not %{bin-available:alectryon}))) \ No newline at end of file +; (rule +; (target dummy) +; (action (progn +; (echo "Alectryon not installed: skipping examples/rocq_proof\n") +; (write-file dummy ""))) +; (enabled_if (not %{bin-available:alectryon}))) From c7b021e61d580b6061f0b040ca04d8e1b40e9de4 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Sat, 17 Jan 2026 19:27:00 +0100 Subject: [PATCH 17/23] Rocq9: rename coqchk to rocqchk --- .github/workflows/ci.yml | 4 ++-- examples/rocq_proof/dune | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 13733eb..1f691d7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -78,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/examples/rocq_proof/dune b/examples/rocq_proof/dune index adb2424..5ac9eec 100644 --- a/examples/rocq_proof/dune +++ b/examples/rocq_proof/dune @@ -1,4 +1,4 @@ -; LATER: re-enable when Alectryon supports Coq 9.0 +; LATER: re-enable when Alectryon supports Rocq 9.0 ; (rule ; (target Example.html) ; (deps (package warblre) (:input (file Example.v))) From 409c6b950c420a80a02f7e9a38d270effbb676e1 Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Wed, 28 Jan 2026 11:22:27 -0500 Subject: [PATCH 18/23] Suppress example output --- mechanization/spec/Inst.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mechanization/spec/Inst.v b/mechanization/spec/Inst.v index 9c83448..9d7e6fd 100644 --- a/mechanization/spec/Inst.v +++ b/mechanization/spec/Inst.v @@ -551,6 +551,7 @@ Notation "$$ s" := (string_of_String s) (at level 0). 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". *) From b17dab019b457279df3536af711a9f05d0f655f6 Mon Sep 17 00:00:00 2001 From: Noe De Santo Date: Wed, 28 Jan 2026 11:29:57 -0500 Subject: [PATCH 19/23] Bump nixpkgs --- .nix/vsrocq-language-server.nix | 5 +++-- flake.lock | 6 +++--- flake.nix | 4 ++-- package-lock.json | 1 + 4 files changed, 9 insertions(+), 7 deletions(-) diff --git a/.nix/vsrocq-language-server.nix b/.nix/vsrocq-language-server.nix index 80f602d..62dc56b 100644 --- a/.nix/vsrocq-language-server.nix +++ b/.nix/vsrocq-language-server.nix @@ -36,7 +36,6 @@ ocamlPackages.buildDunePackage { ++ (with ocamlPackages; [ findlib lablgtk3-sourceview3 - yojson zarith ppx_inline_test ppx_assert @@ -44,7 +43,9 @@ ocamlPackages.buildDunePackage { ppx_deriving ppx_import sexplib - ppx_yojson_conv + (ppx_yojson_conv.override { + ppx_yojson_conv_lib = ppx_yojson_conv_lib.override { yojson = yojson_2; }; + }) lsp sel ppx_optcomp diff --git a/flake.lock b/flake.lock index b08b7ef..524b2b1 100644 --- a/flake.lock +++ b/flake.lock @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1764242076, - "narHash": "sha256-sKoIWfnijJ0+9e4wRvIgm/HgE27bzwQxcEmo2J/gNpI=", + "lastModified": 1769461804, + "narHash": "sha256-msG8SU5WsBUfVVa/9RPLaymvi5bI8edTavbIq3vRlhI=", "owner": "nixos", "repo": "nixpkgs", - "rev": "2fad6eac6077f03fe109c4d4eb171cf96791faa4", + "rev": "bfc1b8a4574108ceef22f02bafcf6611380c100d", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 9d6daf2..517b540 100644 --- a/flake.nix +++ b/flake.nix @@ -16,7 +16,7 @@ let pkgs = nixpkgs.legacyPackages.${system}; - oPkgs = pkgs.ocaml-ng.ocamlPackages_4_14; + oPkgs = pkgs.rocq-core_9_1.ocamlPackages; spec-diff = pkgs.writeShellApplication { name = "spec-diff"; @@ -35,7 +35,7 @@ rocqPackages_9_1.rocq-core rocqPackages_9_1.stdlib (rocqPackages_9_1.callPackage .nix/vsrocq-language-server.nix {}) - + # TODO: switch back to the packages in nixpkgs once the features we need get released oPkgs.ocaml (oPkgs.callPackage .nix/dune.nix {}) diff --git a/package-lock.json b/package-lock.json index 2b8ee4d..a961d15 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1427,6 +1427,7 @@ "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", From 5cc023fc500435123279968d71322bad665cf5bc Mon Sep 17 00:00:00 2001 From: shilangyu Date: Thu, 29 Jan 2026 17:05:40 +0100 Subject: [PATCH 20/23] Test Rocq 9.0 on CI and bump Node version --- .github/workflows/ci.yml | 4 ++-- README.md | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1f691d7..efd8bbe 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -14,8 +14,8 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - rocq: [ "9.1.0" ] - 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 diff --git a/README.md b/README.md index d37b38d..acb49eb 100644 --- a/README.md +++ b/README.md @@ -30,7 +30,7 @@ The mechanization has the following properties: 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 From 2a7507fd33ca348e4e777f27d9e0a8e8cdd33ccc Mon Sep 17 00:00:00 2001 From: shilangyu Date: Sun, 22 Feb 2026 18:02:09 +0100 Subject: [PATCH 21/23] Re-enable Alectryon with vsrocqtop --- .github/pip-requirements.txt | 2 +- .github/workflows/ci.yml | 2 ++ README.md | 9 ++++++++- examples/rocq_proof/dune | 25 ++++++++++++------------- specification_check/rocq_parser.py | 4 ++-- 5 files changed, 25 insertions(+), 17 deletions(-) diff --git a/.github/pip-requirements.txt b/.github/pip-requirements.txt index 19d92e4..0defc4b 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@next git+https://github.com/epfl-systemf/SpecMerger requests == 2.32.4 beautifulsoup4 == 4.12.3 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index efd8bbe..4f4a5f8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -64,6 +64,8 @@ jobs: echo "::group::Install opam packages" opam pin add -n -k version coq ${{ matrix.rocq }} opam install --confirm-level=unsafe-yes --deps-only . + # vsrocqtop is needed by Alectryon + opam install --confirm-level=unsafe-yes vsrocq-language-server echo "::endgroup::" echo "::group::Print opam config (post-install)" diff --git a/README.md b/README.md index acb49eb..418e8bf 100644 --- a/README.md +++ b/README.md @@ -37,6 +37,13 @@ The mechanization has the following properties: 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 [vsrocqtop](https://github.com/rocq-prover/vsrocq). + ``` + opam install vsrocq-language-server + ``` + Alternatively, a [nix](https://nixos.org/) flake installing all the dependencies is provided: ``` nix develop @@ -48,7 +55,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/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. +- `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. Alternatively, if you installed Alectryon, you can open the generated [webpage](_build/default/examples/rocq_proof/Example.html) in your web browser. ## Structure of the repository diff --git a/examples/rocq_proof/dune b/examples/rocq_proof/dune index 5ac9eec..24b6e59 100644 --- a/examples/rocq_proof/dune +++ b/examples/rocq_proof/dune @@ -1,14 +1,13 @@ -; LATER: re-enable when Alectryon supports Rocq 9.0 -; (rule -; (target Example.html) -; (deps (package warblre) (:input (file Example.v))) -; (action -; (run alectryon -Q ../../mechanization Warblre --long-line-threshold -1 %{input})) -; (enabled_if %{bin-available:alectryon})) +(rule + (target Example.html) + (deps (package warblre) (:input (file Example.v))) + (action + (run alectryon --coq-driver vsrocq -Q ../../mechanization Warblre --long-line-threshold -1 %{input})) + (enabled_if %{bin-available:alectryon})) -; (rule -; (target dummy) -; (action (progn -; (echo "Alectryon not installed: skipping examples/rocq_proof\n") -; (write-file dummy ""))) -; (enabled_if (not %{bin-available:alectryon}))) +(rule + (target dummy) + (action (progn + (echo "Alectryon not installed: skipping examples/rocq_proof\n") + (write-file dummy ""))) + (enabled_if (not %{bin-available:alectryon}))) diff --git a/specification_check/rocq_parser.py b/specification_check/rocq_parser.py index 8876614..6bbb864 100644 --- a/specification_check/rocq_parser.py +++ b/specification_check/rocq_parser.py @@ -4,7 +4,7 @@ from dataclasses import dataclass from typing import Dict, List, Tuple -from alectryon.literate import Comment, StringView, coq_partition +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 @@ -96,7 +96,7 @@ def __process_lines(self, rocq_code, all_filenames, matcher: re.Pattern) -> list comments = [] for filename in all_filenames: file = rocq_code[filename] - partition = coq_partition(file) + partition = CoqParser(file).partition() for field in partition: if isinstance(field, Comment) and matcher.match(str(field.v)): start_line_num = ROCQParser.__get_line_num(field.v) From 1657babedb991424e225d689c3ee8b0e151e9f5d Mon Sep 17 00:00:00 2001 From: shilangyu Date: Mon, 23 Feb 2026 09:09:25 +0100 Subject: [PATCH 22/23] Fix Alectryon example --- .github/pip-requirements.txt | 2 +- .github/workflows/ci.yml | 3 +-- examples/rocq_proof/Example.v | 11 +++++++---- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/.github/pip-requirements.txt b/.github/pip-requirements.txt index 0defc4b..c26e924 100644 --- a/.github/pip-requirements.txt +++ b/.github/pip-requirements.txt @@ -1,4 +1,4 @@ -alectryon @ git+https://github.com/cpitclaudel/alectryon@next +alectryon @ git+https://github.com/cpitclaudel/alectryon@a02a99c75c4166efc8812a600e8cbf4588424c0f git+https://github.com/epfl-systemf/SpecMerger requests == 2.32.4 beautifulsoup4 == 4.12.3 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4f4a5f8..0bc8301 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -63,9 +63,8 @@ jobs: echo "::group::Install opam packages" opam pin add -n -k version coq ${{ matrix.rocq }} - opam install --confirm-level=unsafe-yes --deps-only . # vsrocqtop is needed by Alectryon - opam install --confirm-level=unsafe-yes vsrocq-language-server + opam install --confirm-level=unsafe-yes --deps-only . vsrocq-language-server echo "::endgroup::" echo "::group::Print opam config (post-install)" diff --git a/examples/rocq_proof/Example.v b/examples/rocq_proof/Example.v index 9c9f8ac..8736506 100644 --- a/examples/rocq_proof/Example.v +++ b/examples/rocq_proof/Example.v @@ -56,17 +56,20 @@ Section AbstractMatching. Definition compilation_result := Semantics.compilePattern regex_of_interest rer. - Lemma compiles_successfully: + Lemma compiles_successfully_refl: exists m, compilation_result = Result.Success m. Proof. (** Again, since the regex is concrete, we can just compute. **) eexists. cbn. reflexivity. + Qed. - (** But we can also use some theorems from the development, which would work even if the regex was left more abstract. **) - Restart. + (** But we can also use some theorems from the development, which would work even if the regex was left more abstract: **) - Search Semantics.compilePattern Result.Success. + Search Semantics.compilePattern Result.Success. + Lemma compiles_successfully_thm: + exists m, compilation_result = Result.Success m. + Proof. (** We use the theorem listed in section 4.2.1 in the paper, [compilePattern_success], which states that compilation always succeeds if a regex passes early error checks. **) apply compilePattern_success. - (** We have to show that the number of groups per [rer] matches the actual number From 6bbf25e97d258d6a7b748bec3e33e83ccdab4ad7 Mon Sep 17 00:00:00 2001 From: shilangyu Date: Mon, 23 Feb 2026 11:08:26 +0100 Subject: [PATCH 23/23] Remove Alectryon --- .github/workflows/ci.yml | 3 +-- README.md | 8 +------- examples/dune-project | 6 ++++-- examples/rocq_proof/dune | 18 ++++++------------ 4 files changed, 12 insertions(+), 23 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0bc8301..efd8bbe 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -63,8 +63,7 @@ jobs: echo "::group::Install opam packages" opam pin add -n -k version coq ${{ matrix.rocq }} - # vsrocqtop is needed by Alectryon - opam install --confirm-level=unsafe-yes --deps-only . vsrocq-language-server + opam install --confirm-level=unsafe-yes --deps-only . echo "::endgroup::" echo "::group::Print opam config (post-install)" diff --git a/README.md b/README.md index 418e8bf..5c06232 100644 --- a/README.md +++ b/README.md @@ -37,12 +37,6 @@ The mechanization has the following properties: 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 [vsrocqtop](https://github.com/rocq-prover/vsrocq). - ``` - opam install vsrocq-language-server - ``` 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/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. Alternatively, if you installed Alectryon, you can open the generated [webpage](_build/default/examples/rocq_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 diff --git a/examples/dune-project b/examples/dune-project index 102013f..d5252f5 100644 --- a/examples/dune-project +++ b/examples/dune-project @@ -1,12 +1,14 @@ -(lang dune 3.14) +(lang dune 3.21) ; This package is defined in a sub dune-project to prevent the installation of example executables (generate_opam_files false) +(using rocq 0.11) (using melange 0.1) (using directory-targets 0.1) (package (name warblre-examples) (depends - warblre-engines)) + warblre-engines + warblre)) diff --git a/examples/rocq_proof/dune b/examples/rocq_proof/dune index 24b6e59..c0d92fe 100644 --- a/examples/rocq_proof/dune +++ b/examples/rocq_proof/dune @@ -1,13 +1,7 @@ -(rule - (target Example.html) - (deps (package warblre) (:input (file Example.v))) - (action - (run alectryon --coq-driver vsrocq -Q ../../mechanization Warblre --long-line-threshold -1 %{input})) - (enabled_if %{bin-available:alectryon})) +(include_subdirs qualified) -(rule - (target dummy) - (action (progn - (echo "Alectryon not installed: skipping examples/rocq_proof\n") - (write-file dummy ""))) - (enabled_if (not %{bin-available:alectryon}))) +(rocq.theory + (name Example) + (package warblre-examples) + (generate_project_file) + (theories Stdlib Warblre))