Merge pull request #693 from LPCIC/support-multiple-elpi-version

ifdefs on elpi version in source code

.github/workflows/nix-action-coq-8.20.yml

@@ -1,4 +1,126 @@
 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
+    - 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

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"24e96b4870378d5e87fd2d0dd46405b471c286ab"
+"42eecc8a0f642b84bd179859d708ddc710c92004"

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}

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))

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 ()

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

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))