From 742a02333c3f7fed5358cf35420bf7c96bcd1205 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Sep 2024 10:52:01 +0200 Subject: [PATCH 1/4] ifdefs on elpi version in source code --- coq-elpi.opam | 2 +- etc/dune | 7 +++++++ etc/version_parser.ml | 17 +++++++++++++++++ src/coq_elpi_builtins_synterp.ml | 10 +++++++++- src/dune | 14 ++++++++++++++ 5 files changed, 48 insertions(+), 2 deletions(-) create mode 100644 etc/version_parser.ml diff --git a/coq-elpi.opam b/coq-elpi.opam index b14ef6f82..9c20beef8 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -19,7 +19,7 @@ depends: [ "ocaml" {>= "4.10.0"} "stdlib-shims" "elpi" {>= "1.18.2" & < "1.20.0~"} - "coq" {>= "8.20" & < "8.21"} + "coq" {>= "8.20+rc1" & < "8.21~"} "ppx_optcomp" "ocaml-lsp-server" {with-dev-setup} "odoc" {with-doc} diff --git a/etc/dune b/etc/dune index 3e8618d5a..461eb00af 100644 --- a/etc/dune +++ b/etc/dune @@ -9,4 +9,11 @@ (public_name coq_elpi_optcomp) (modules optcomp) (libraries str) + (package coq-elpi)) + +(executable + (name version_parser) + (public_name coq_elpi_version_parser) + (modules version_parser) + (libraries str) (package coq-elpi)) \ No newline at end of file diff --git a/etc/version_parser.ml b/etc/version_parser.ml new file mode 100644 index 000000000..1b9cf761d --- /dev/null +++ b/etc/version_parser.ml @@ -0,0 +1,17 @@ + +let is_number x = try let _ = int_of_string x in true with _ -> false ;; + +let main () = + let v = Sys.argv.(1) in + let l = String.split_on_char '.' Str.(replace_first (regexp "^v") "" v) in + (* sanitization *) + let l = + match l with + | l when List.for_all is_number l -> l + | ["%%VERSION_NUM%%"] -> ["99";"99";"99"] + | _ -> Printf.eprintf "version_parser: cannot parse: %s\n" v; exit 1 in + let open Format in + printf "(%a)%!" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp_print_string) l +;; + +main () \ No newline at end of file diff --git a/src/coq_elpi_builtins_synterp.ml b/src/coq_elpi_builtins_synterp.ml index ecbf203e9..5324fd132 100644 --- a/src/coq_elpi_builtins_synterp.ml +++ b/src/coq_elpi_builtins_synterp.ml @@ -2,6 +2,8 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) +[%%import "coq_elpi_config.mlh"] + module API = Elpi.API module State = API.State module Conv = API.Conversion @@ -150,6 +152,12 @@ let invocation_site_loc_synterp : API.Ast.Loc.t State.component = ~init:(fun () -> API.Ast.Loc.initial "(should-not-happen)") ~start:(fun x -> x) () +[%%if elpi >= (1, 20, 0)] +let compat_graft x = x +[%%else] +let compat_graft = Option.map (function `Remove, _ -> nYI "clause removal" | ((`Replace | `Before | `After), _) as x -> x) +[%%endif] + type accumulation_item = qualified_name * API.Ast.program * Id.t list * Coq_elpi_utils.clause_scope let accumulate_clauses ~clauses_for_later ~accumulate_to_db ~preprocess_clause ~scope ~dbname clauses ~depth ~options state = let invocation_loc = State.get invocation_site_loc_synterp state in @@ -158,7 +166,7 @@ let accumulate_clauses ~clauses_for_later ~accumulate_to_db ~preprocess_clause ~ let clauses scope = clauses |> CList.rev_map (fun (name,graft,clause) -> let vars, clause = preprocess_clause ~depth clause in - let graft = Option.map (function `Remove, _ -> nYI "clause removal" | ((`Replace | `Before | `After), _) as x -> x) graft in + let graft = compat_graft graft in let clause = U.clause_of_term ?name ?graft ~depth loc clause in (dbname,clause,vars,scope)) in let local = (options : options).local = Some true in diff --git a/src/dune b/src/dune index ef9a8d9de..ef6641bb5 100644 --- a/src/dune +++ b/src/dune @@ -3,6 +3,7 @@ (public_name coq-elpi.elpi) (synopsis "Elpi") (flags :standard -w -27) + (preprocessor_deps coq_elpi_config.mlh) (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) (libraries coq-core.plugins.ltac coq-core.vernac elpi)) @@ -30,7 +31,20 @@ (target coq_elpi_config.ml) (action (with-stdout-to %{target} (progn + (echo "(* Automatically generated, don't edit *)\n") + (echo "[%%import \"coq_elpi_config.mlh\"]\n") + (echo "let elpi_version = \"%{version:elpi}\"\n") (echo "let elpi2html = \"%{lib:elpi:elpi2html.elpi}\";;"))))) +(rule + (target coq_elpi_config.mlh) + (action (with-stdout-to %{target} + (progn + (echo "(* Automatically generated, don't edit *)\n") + (echo "[%%define elpi ") + (run coq_elpi_version_parser %{version:elpi}) + (echo "]\n"))))) + + (coq.pp (modules coq_elpi_vernacular_syntax coq_elpi_arg_syntax)) From 2e75f4e9f2d605c0d0e66adc24f6d473435108bf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Sep 2024 10:45:14 +0200 Subject: [PATCH 2/4] nix --- .github/workflows/nix-action-coq-8.20.yml | 57 +++++++++++++++++++++++ .nix/coq-nix-toolbox.nix | 2 +- 2 files changed, 58 insertions(+), 1 deletion(-) diff --git a/.github/workflows/nix-action-coq-8.20.yml b/.github/workflows/nix-action-coq-8.20.yml index b40e380e4..cffab76ce 100644 --- a/.github/workflows/nix-action-coq-8.20.yml +++ b/.github/workflows/nix-action-coq-8.20.yml @@ -1,4 +1,61 @@ jobs: + autosubst: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target autosubst + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.20\" --argstr job \"autosubst\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "autosubst" coq: needs: [] runs-on: ubuntu-latest diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 9b872206b..02b5e945e 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"24e96b4870378d5e87fd2d0dd46405b471c286ab" +"b472641a6662a06901b280845b1473e7d6b08ab5" From 148ecb76651293960cb67eb67e038d87e2592a62 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Sep 2024 10:50:42 +0200 Subject: [PATCH 3/4] Update etc/version_parser.ml --- etc/version_parser.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/etc/version_parser.ml b/etc/version_parser.ml index 1b9cf761d..af8681bb8 100644 --- a/etc/version_parser.ml +++ b/etc/version_parser.ml @@ -8,7 +8,7 @@ let main () = let l = match l with | l when List.for_all is_number l -> l - | ["%%VERSION_NUM%%"] -> ["99";"99";"99"] + | ( [""] | ["%%VERSION_NUM%%"] ) -> ["99";"99";"99"] | _ -> Printf.eprintf "version_parser: cannot parse: %s\n" v; exit 1 in let open Format in printf "(%a)%!" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp_print_string) l From d961ac6caf54efb1c66a8eeac77e49dda4b9b2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Sep 2024 22:47:06 +0200 Subject: [PATCH 4/4] nix --- .github/workflows/nix-action-coq-8.20.yml | 65 +++++++++++++++++++++++ .nix/coq-nix-toolbox.nix | 2 +- 2 files changed, 66 insertions(+), 1 deletion(-) diff --git a/.github/workflows/nix-action-coq-8.20.yml b/.github/workflows/nix-action-coq-8.20.yml index cffab76ce..ca320c749 100644 --- a/.github/workflows/nix-action-coq-8.20.yml +++ b/.github/workflows/nix-action-coq-8.20.yml @@ -1,4 +1,69 @@ jobs: + QuickChick: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target QuickChick + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.20\" --argstr job \"QuickChick\" \\\n --dry-run 2>&1 >\ + \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-ext-lib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "coq-ext-lib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: simple-io' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "simple-io" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "QuickChick" autosubst: needs: - coq diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 02b5e945e..657441985 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"b472641a6662a06901b280845b1473e7d6b08ab5" +"42eecc8a0f642b84bd179859d708ddc710c92004"