diff --git a/.github/workflows/nix-action-rocq-9.2.yml b/.github/workflows/nix-action-rocq-9.2.yml index d3532d4261..bb495a572f 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -2,6 +2,72 @@ concurrency: cancel-in-progress: true group: ${{ github.workflow }}-${{ github.ref }} jobs: + bignums: + needs: + - rocq-core + - stdlib + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (bignums) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.2\" --argstr job \"bignums\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "bignums" coq: needs: - rocq-core @@ -63,6 +129,72 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" + flocq: + needs: + - coq + - stdlib + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (flocq) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.2\" --argstr job \"flocq\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "flocq" hierarchy-builder: needs: - rocq-core @@ -327,6 +459,7 @@ jobs: stdlib: needs: - rocq-core + - micromega-plugin runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -381,6 +514,10 @@ jobs: name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.github/workflows/nix-action-rocq-9.3.yml b/.github/workflows/nix-action-rocq-9.3.yml index 5a65fd0f63..f91ea30766 100644 --- a/.github/workflows/nix-action-rocq-9.3.yml +++ b/.github/workflows/nix-action-rocq-9.3.yml @@ -2,6 +2,72 @@ concurrency: cancel-in-progress: true group: ${{ github.workflow }}-${{ github.ref }} jobs: + bignums: + needs: + - rocq-core + - stdlib + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (bignums) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.3\" --argstr job \"bignums\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "bignums" coq: needs: - rocq-core @@ -63,6 +129,72 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.3" --argstr job "coq" + flocq: + needs: + - coq + - stdlib + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (flocq) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.3\" --argstr job \"flocq\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "flocq" hierarchy-builder: needs: - rocq-core @@ -327,6 +459,7 @@ jobs: stdlib: needs: - rocq-core + - micromega-plugin runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -381,6 +514,10 @@ jobs: name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.3" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index 4df8f1c552..af0fa25ceb 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -360,6 +360,7 @@ jobs: stdlib: needs: - rocq-core + - micromega-plugin runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -414,6 +415,10 @@ jobs: name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.nix/config.nix b/.nix/config.nix index 25d6951cdf..658962ebca 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -84,12 +84,22 @@ with builtins; with (import {}).lib; common-bundles = listToAttrs (forEach master (p: { name = p; value.override.version = "master"; })) // { + aac-tactics.job = false; + ceres.job = false; CertiRocq.job = false; + Cheerios.job = false; CoLoR.job = false; ConCert.job = false; coqeal.job = false; + coq-hammer.job = false; + coq-hammer-tactics.job = false; + coqutil.job = false; + equations.job = false; + ExtLib.job = false; fourcolor.job = false; gaia.job = false; + InfSeqExt.job = false; + iris.job = false; mathcomp.job = false; mathcomp-algebra.job = true; mathcomp-analysis.job = false; @@ -103,10 +113,16 @@ with builtins; with (import {}).lib; mathcomp-real-closed.job = false; mathcomp-solvable.job = false; mathcomp-field.job = false; + MenhirLib.job = false; multinomials.job = false; libvalidsdp.job = false; odd-order.job = false; + Ordinal.job = false; + paco.job = false; parseque.job = false; + rewriter.job = false; + stdpp.job = false; + StructTact.job = false; validsdp.job = false; wasmcert.job = false; # To add an overlay applying to all bundles, @@ -118,6 +134,7 @@ with builtins; with (import {}).lib; # for a complete list of Coq packages available in Nix # * : is such that this will use the branch # from https://github.com// + stdlib.override.version = "proux01:tify"; }; in { "rocq-master".rocqPackages = common-bundles // { diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 71ff6cb1b7..a99e723bae 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"f0c74efcec0d8657e1d5bcc6fd431b7caee1e43d" +"15e41de5ef219a79d92360bd51a924b12426aad2" diff --git a/default.nix b/default.nix index 0c05a14189..102d8413b6 100644 --- a/default.nix +++ b/default.nix @@ -4,8 +4,8 @@ bundle ? null, job ? null, inNixShell ? null, src ? ./., }@args: let auto = fetchGit { - url = "https://github.com/rocq-community/coq-nix-toolbox.git"; - ref = "master"; + url = "https://github.com/proux01/coq-nix-toolbox.git"; + ref = "micromega"; rev = import .nix/coq-nix-toolbox.nix; }; in diff --git a/src/dune b/src/dune index d9d661e133..7f8102a742 100644 --- a/src/dune +++ b/src/dune @@ -1,19 +1,19 @@ (library (name micromega_ml_plugin) - (modules (:standard \ csdpcert g_zify zify)) - (public_name rocq-micromega-plugin.plugin) + (modules (:standard \ csdpcert g_tify tify)) + (public_name rocq-micromega-plugin.plugin) (flags :standard -w -27) (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac)) (library - (name zify_ml_plugin) - (public_name rocq-micromega-plugin.zify) - (modules g_zify zify) + (name tify_ml_plugin) + (public_name rocq-micromega-plugin.tify) + (modules g_tify tify) (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac)) (coq.pp - (modules g_micromega g_zify)) + (modules g_micromega g_tify)) diff --git a/src/g_tify.mlg b/src/g_tify.mlg new file mode 100644 index 0000000000..1242b23e6c --- /dev/null +++ b/src/g_tify.mlg @@ -0,0 +1,150 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Pp.(str "The tactic " ++ str zify_tac ++ str " is deprecated. Use " ++ str tify_tac ++ str " instead.")) + +let deprecate_zify_vernac cmd1 cmd2 = + CWarnings.create ~category:depr_since_mp_1_0 + ~name:("deprecated-"^cmd1^"-Zify-"^cmd2) + (fun () -> Pp.( + str cmd1 ++ str " Zify "++ str cmd2 ++ str " is deprecated. Use "++ str cmd1 ++ str " Tify "++ str cmd2 ++ str " instead.")) + +let deprecate_zify_iter_specs = deprecate_zify_tac "zify_iter_specs" "tify_iter_specs" +let deprecate_zify_iter_let = deprecate_zify_tac "zify_iter_let" "tify_iter_let" +let deprecate_zify_elim_let = deprecate_zify_tac "zify_elim_let" "tify_elim_let" +let deprecate_zify_op = deprecate_zify_tac "zify_op" "tify_op Z" +let deprecate_zify_saturate = deprecate_zify_tac "zify_saturate" "tify_saturate" + +let deprecate_Add_InjTyp = deprecate_zify_vernac "Add" "InjTyp" +let deprecate_Add_BinOp = deprecate_zify_vernac "Add" "BinOp" +let deprecate_Add_UnOp = deprecate_zify_vernac "Add" "UnOp" +let deprecate_Add_CstOp = deprecate_zify_vernac "Add" "CstOp" +let deprecate_Add_BinRel = deprecate_zify_vernac "Add" "BinRel" +let deprecate_Add_PropOp = deprecate_zify_vernac "Add" "PropOp" +let deprecate_Add_PropBinOp = deprecate_zify_vernac "Add" "PropBinOp" +let deprecate_Add_PropUOp = deprecate_zify_vernac "Add" "PropUOp" +let deprecate_Add_BinOpSpec = deprecate_zify_vernac "Add" "BinOpSpec" +let deprecate_Add_UnOpSpec = deprecate_zify_vernac "Add" "UnOpSpec" +let deprecate_Add_Saturate = deprecate_zify_vernac "Add" "Saturate" + +let deprecate_Show_InjTyp = deprecate_zify_vernac "Show" "InjTyp" +let deprecate_Show_BinOp = deprecate_zify_vernac "Show" "BinOp" +let deprecate_Show_UnOp = deprecate_zify_vernac "Show" "UnOp" +let deprecate_Show_CstOp = deprecate_zify_vernac "Show" "CstOp" +let deprecate_Show_BinRel = deprecate_zify_vernac "Show" "BinRel" +let deprecate_Show_BinOpSpec = deprecate_zify_vernac "Show" "BinOpSpec" +let deprecate_Show_UnOpSpec = deprecate_zify_vernac "Show" "UnOpSpec" + +} + +DECLARE PLUGIN "rocq-micromega-plugin.tify" + +VERNAC COMMAND EXTEND DECLAREZIFYINJECTION CLASSIFIED AS SIDEFF +| #[ locality ] ["Add" "Zify" "InjTyp" reference(t) ] -> { + deprecate_Add_InjTyp (); Tify.InjTable.register locality t } +| #[ locality ] ["Add" "Zify" "BinOp" reference(t) ] -> { + deprecate_Add_BinOp (); Tify.BinOp.register locality t } +| #[ locality ] ["Add" "Zify" "UnOp" reference(t) ] -> { + deprecate_Add_UnOp (); Tify.UnOp.register locality t } +| #[ locality ] ["Add" "Zify" "CstOp" reference(t) ] -> { + deprecate_Add_CstOp (); Tify.CstOp.register locality t } +| #[ locality ] ["Add" "Zify" "BinRel" reference(t) ] -> { + deprecate_Add_BinRel (); Tify.BinRel.register locality t } +| #[ locality ] ["Add" "Zify" "PropOp" reference(t) ] -> { + deprecate_Add_PropOp (); Tify.PropBinOp.register locality t } +| #[ locality ] ["Add" "Zify" "PropBinOp" reference(t) ] -> { + deprecate_Add_PropBinOp (); Tify.PropBinOp.register locality t } +| #[ locality ] ["Add" "Zify" "PropUOp" reference(t) ] -> { + deprecate_Add_PropUOp (); Tify.PropUnOp.register locality t } +| #[ locality ] ["Add" "Zify" "BinOpSpec" reference(t) ] -> { + deprecate_Add_BinOpSpec (); Tify.BinOpSpec.register locality t } +| #[ locality ] ["Add" "Zify" "UnOpSpec" reference(t) ] -> { + deprecate_Add_UnOpSpec (); Tify.UnOpSpec.register locality t } +| #[ locality ] ["Add" "Zify" "Saturate" reference(t) ] -> { + deprecate_Add_Saturate (); Tify.Saturate.register locality t } +END + +VERNAC COMMAND EXTEND TIFYDECLAREINJECTION CLASSIFIED AS SIDEFF +| #[ locality ] ["Add" "Tify" "InjTyp" reference(t) ] -> { Tify.InjTable.register locality t } +| #[ locality ] ["Add" "Tify" "BinOp" reference(t) ] -> { Tify.BinOp.register locality t } +| #[ locality ] ["Add" "Tify" "UnOp" reference(t) ] -> { Tify.UnOp.register locality t } +| #[ locality ] ["Add" "Tify" "CstOp" reference(t) ] -> { Tify.CstOp.register locality t } +| #[ locality ] ["Add" "Tify" "BinRel" reference(t) ] -> { Tify.BinRel.register locality t } +| #[ locality ] ["Add" "Tify" "PropOp" reference(t) ] -> { Tify.PropBinOp.register locality t } +| #[ locality ] ["Add" "Tify" "PropBinOp" reference(t) ] -> { Tify.PropBinOp.register locality t } +| #[ locality ] ["Add" "Tify" "PropUOp" reference(t) ] -> { Tify.PropUnOp.register locality t } +| #[ locality ] ["Add" "Tify" "BinOpSpec" reference(t) ] -> { Tify.BinOpSpec.register locality t } +| #[ locality ] ["Add" "Tify" "UnOpSpec" reference(t) ] -> { Tify.UnOpSpec.register locality t } +| #[ locality ] ["Add" "Tify" "Saturate" reference(t) ] -> { Tify.Saturate.register locality t } +END + + +TACTIC EXTEND ITER +| [ "zify_iter_specs"] -> { + deprecate_zify_iter_specs (); Tify.iter_specs} +| [ "tify_iter_specs"] -> { Tify.iter_specs} +END + +TACTIC EXTEND TRANS +| [ "zify_op" ] -> { + deprecate_zify_op () ; Tify.zify_op ()} +| [ "zify_saturate" ] -> { + deprecate_zify_saturate () ; Tify.saturate } +| [ "zify_iter_let" tactic(t)] -> { + deprecate_zify_iter_let (); Tify.iter_let t } +| [ "zify_elim_let" ] -> { + deprecate_zify_elim_let (); Tify.elim_let } +| [ "tify_op" reference(t) ] -> { Tify.tify_op t} +| [ "tify_saturate" ] -> { Tify.saturate } +| [ "tify_elim_let" ] -> { Tify.elim_let } +| [ "tify_iter_let" tactic(t)] -> { Tify.iter_let t } +END + +VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF +|[ "Show" "Zify" "InjTyp" ] -> { + deprecate_Show_InjTyp (); Tify.InjTable.print () } +|[ "Show" "Zify" "BinOp" ] -> { + deprecate_Show_BinOp (); Tify.BinOp.print () } +|[ "Show" "Zify" "UnOp" ] -> { + deprecate_Show_UnOp (); Tify.UnOp.print () } +|[ "Show" "Zify" "CstOp"] -> { + deprecate_Show_CstOp (); Tify.CstOp.print () } +|[ "Show" "Zify" "BinRel"] -> { + deprecate_Show_BinRel (); Tify.BinRel.print () } +|[ "Show" "Zify" "UnOpSpec"] -> { + deprecate_Show_UnOpSpec (); Tify.UnOpSpec.print() } +|[ "Show" "Zify" "BinOpSpec"] -> { + deprecate_Show_BinOpSpec (); Tify.BinOpSpec.print() } +END + +VERNAC COMMAND EXTEND TifyPrint CLASSIFIED AS SIDEFF +|[ "Show" "Tify" "InjTyp" ] -> { Tify.InjTable.print () } +|[ "Show" "Tify" "BinOp" ] -> { Tify.BinOp.print () } +|[ "Show" "Tify" "UnOp" ] -> { Tify.UnOp.print () } +|[ "Show" "Tify" "CstOp"] -> { Tify.CstOp.print () } +|[ "Show" "Tify" "BinRel"] -> { Tify.BinRel.print () } +|[ "Show" "Tify" "UnOpSpec"] -> { Tify.UnOpSpec.print() } +|[ "Show" "Tify" "BinOpSpec"] -> { Tify.BinOpSpec.print() } +END diff --git a/src/g_zify.mli b/src/g_tify.mli similarity index 100% rename from src/g_zify.mli rename to src/g_tify.mli diff --git a/src/g_zify.mlg b/src/g_zify.mlg deleted file mode 100644 index 5c997b74ea..0000000000 --- a/src/g_zify.mlg +++ /dev/null @@ -1,56 +0,0 @@ -(************************************************************************) -(* * The Rocq Prover / The Rocq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* { Zify.InjTable.register locality t } -| #[ locality ] ["Add" "Zify" "BinOp" reference(t) ] -> { Zify.BinOp.register locality t } -| #[ locality ] ["Add" "Zify" "UnOp" reference(t) ] -> { Zify.UnOp.register locality t } -| #[ locality ] ["Add" "Zify" "CstOp" reference(t) ] -> { Zify.CstOp.register locality t } -| #[ locality ] ["Add" "Zify" "BinRel" reference(t) ] -> { Zify.BinRel.register locality t } -| #[ locality ] ["Add" "Zify" "PropOp" reference(t) ] -> { Zify.PropBinOp.register locality t } -| #[ locality ] ["Add" "Zify" "PropBinOp" reference(t) ] -> { Zify.PropBinOp.register locality t } -| #[ locality ] ["Add" "Zify" "PropUOp" reference(t) ] -> { Zify.PropUnOp.register locality t } -| #[ locality ] ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register locality t } -| #[ locality ] ["Add" "Zify" "UnOpSpec" reference(t) ] -> { Zify.UnOpSpec.register locality t } -| #[ locality ] ["Add" "Zify" "Saturate" reference(t) ] -> { Zify.Saturate.register locality t } -END - -TACTIC EXTEND ITER -| [ "zify_iter_specs"] -> { Zify.iter_specs} -END - -TACTIC EXTEND TRANS -| [ "zify_op" ] -> { Zify.zify_tac } -| [ "zify_saturate" ] -> { Zify.saturate } -| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t } -| [ "zify_elim_let" ] -> { Zify.elim_let } -END - -VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF -|[ "Show" "Zify" "InjTyp" ] -> { Zify.InjTable.print () } -|[ "Show" "Zify" "BinOp" ] -> { Zify.BinOp.print () } -|[ "Show" "Zify" "UnOp" ] -> { Zify.UnOp.print () } -|[ "Show" "Zify" "CstOp"] -> { Zify.CstOp.print () } -|[ "Show" "Zify" "BinRel"] -> { Zify.BinRel.print () } -|[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() } -|[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() } -END diff --git a/src/zify.ml b/src/tify.ml similarity index 93% rename from src/zify.ml rename to src/tify.ml index ddb33b7d3f..aa476d0dee 100644 --- a/src/zify.ml +++ b/src/tify.ml @@ -18,7 +18,7 @@ module ERelevance = EConstr.ERelevance (* many cases, TODO clean them up someday *) [@@@warning "-unused-field"] -let debug_zify = CDebug.create ~name:"zify-plugin" () +let debug_zify = CDebug.create ~name:"tify-plugin" () (* The following [constr] are necessary for constructing the proof terms *) @@ -40,6 +40,9 @@ let rocq_BinOpSpec () = Rocqlib.lib_ref "ZifyClasses.BinOpSpec" let rocq_UnOpSpec () = Rocqlib.lib_ref "ZifyClasses.UnOpSpec" let rocq_Saturate () = Rocqlib.lib_ref "ZifyClasses.Saturate" +(* Z *) +let rocq_Z = lazy (Rocqlib.lib_ref "num.Z.type") + (* morphism like lemma *) let mkapp2 () = zify "mkapp2" @@ -87,11 +90,6 @@ let get_type_of env evd e = (* arguments are dealt with in a second step *) -let rec find_option pred l = - match l with - | [] -> raise Not_found - | e :: l -> ( match pred e with Some r -> r | None -> find_option pred l ) - module ConstrMap = struct [%%if rocq = "9.0" || rocq = "9.1"] open Names.GlobRef @@ -443,9 +441,9 @@ module type Elt = sig (* val arity : int*) end -let table = Summary.ref ~name:"zify-plugin_table" ConstrMap.empty -let saturate = Summary.ref ~name:"zify-plugin_saturate" ConstrMap.empty -let specs = Summary.ref ~name:"zify-plugin_specs" ConstrMap.empty +let table = Summary.ref ~name:"tify-plugin_table" ConstrMap.empty +let saturate = Summary.ref ~name:"tify-plugin_saturate" ConstrMap.empty +let specs = Summary.ref ~name:"tify-plugin_specs" ConstrMap.empty let table_cache = ref ConstrMap.empty let saturate_cache = ref ConstrMap.empty let specs_cache = ref ConstrMap.empty @@ -734,7 +732,7 @@ module MakeTable (E : Elt) : S = struct let subst_constr (subst, c) = Mod_subst.subst_mps subst c in Libobject.declare_object @@ Libobject.object_with_locality - ("register-zify-plugin-" ^ E.name) + ("register-tify-plugin-" ^ E.name) ~cache:cache_constr ~subst:(Some subst_constr) ~discharge:(fun _ -> assert false) @@ -870,8 +868,7 @@ module CstrTable = struct let hyps_table = HConstr.create 20 in let () = List.iter (fun decl -> HConstr.add hyps_table (NamedDecl.get_type decl) ()) - (EConstr.named_context env) - in + (EConstr.named_context env) in fun c -> let m = HConstr.mem hyps_table c in if not m then HConstr.add hyps_table c (); @@ -1171,12 +1168,44 @@ let classify_prop env evd e = | _ -> OTHEROP (e, [||]) + let check_target_inj evd inj d = match inj , target_inj d with | None , _ -> true | Some _ , None -> false | Some i1 , Some i2 -> EInjT.eq_inj evd i1 i2 +type score = + | FullMatch + | PartialMatch + | NoMatch + +let le_score s1 s2 = + match s1, s2 with + | _ , FullMatch -> true + | FullMatch , _ -> false + | _ , PartialMatch -> true + | PartialMatch, _ -> false + | NoMatch , NoMatch -> true + + +let score_operator pref evd d = + match d with + | BinRel d -> if EConstr.eq_constr evd pref d.deriv.EBinRelT.target + then FullMatch else NoMatch + | BinOp d -> begin + match EConstr.eq_constr evd pref d.deriv.EBinOpT.target1 , + EConstr.eq_constr evd pref d.deriv.EBinOpT.target2 with + | false, false -> NoMatch + | false, true | true,false -> PartialMatch + | true , true -> FullMatch + end + | UnOp d -> + if EConstr.eq_constr evd pref d.deriv.EUnOpT.target1 + then FullMatch else NoMatch + | CstOp d -> FullMatch + | _ -> FullMatch + (** [match_operator env evd hd arg inj (t,d)] - hd is head operator of t @@ -1184,33 +1213,58 @@ let check_target_inj evd inj d = - If t = Application _, then we extract the relevant number of arguments from arg and check for convertibility *) -let match_operator env evd hd args inj (t, d) = - let decomp t i = +let match_operator pref env evd hd args (inj: EInjT.t option) (t, d) = + let decomp s t i = let n = Array.length args in let t' = EConstr.mkApp (hd, Array.sub args 0 (n - i)) in - if is_convertible env evd t' t then Some (d, t) else None + if is_convertible env evd t' t then Some (s, (d, t)) else None in if check_target_inj evd inj d then - match t with - | OtherTerm t -> Some (d, t) - | Application t -> ( - match d with - | CstOp _ -> decomp t 0 - | UnOp _ -> decomp t 1 - | BinOp _ -> decomp t 2 - | BinRel _ -> decomp t 2 - | PropOp _ -> decomp t 2 - | PropUnOp _ -> decomp t 1 - | _ -> None ) + let s = score_operator pref evd d in + match t with + | OtherTerm t -> Some (s, (d, t)) + | Application t -> + (match d with + | CstOp _ -> decomp s t 0 + | UnOp _ -> decomp s t 1 + | BinOp _ -> decomp s t 2 + | BinRel _ -> decomp s t 2 + | PropOp _ -> decomp s t 2 + | PropUnOp _ -> decomp s t 1 + | _ -> None ) else None +let find_best p l = + + let best s r v = + match v with + | None -> Some(s,r) + | Some(s',r') -> if le_score s s' + then v else Some(s,r) in + let get_result v = + match v with + | None -> raise Not_found + | Some(_,r) -> r in + + let rec find res l = + match l with + | [] -> get_result res + | e::l -> match p e with + | None -> find res l + | Some(s',r') -> + if s' = FullMatch then r' + else find (best s' r' res) l in + find None l + + + let pp_trans_expr env evd e res = debug_zify (fun () -> Pp.(str "\ntrans_expr " ++ pp_prf evd e.inj e.constr res)); res -let rec trans_expr env evd e = +let rec trans_expr dtyp env evd e = let inj = e.inj in let e = e.constr in try @@ -1219,7 +1273,7 @@ let rec trans_expr env evd e = else let k, t = find_option - (match_operator env evd c a (Some inj)) + (match_operator dtyp env evd c a (Some inj)) (ConstrMap.find_all env evd c !table_cache) in let n = Array.length a in @@ -1228,7 +1282,7 @@ let rec trans_expr env evd e = ECstOpT.(if c'.is_construct then evd, Term else evd, Prf (c'.cst, c'.cstinj)) | UnOp {deriv = unop} -> let evd, prf = - trans_expr env evd + trans_expr dtyp env evd { constr = a.(n - 1) ; typ = unop.EUnOpT.source1 ; inj = unop.EUnOpT.inj1_t } @@ -1236,13 +1290,13 @@ let rec trans_expr env evd e = app_unop env evd e unop a.(n - 1) prf | BinOp {deriv = binop} -> let evd, prf1 = - trans_expr env evd + trans_expr dtyp env evd { constr = a.(n - 2) ; typ = binop.EBinOpT.source1 ; inj = binop.EBinOpT.inj1 } in let evd, prf2 = - trans_expr env evd + trans_expr dtyp env evd { constr = a.(n - 1) ; typ = binop.EBinOpT.source2 ; inj = binop.EBinOpT.inj2 } @@ -1251,9 +1305,9 @@ let rec trans_expr env evd e = | d -> evd, mkvar evd inj e with Not_found | DestKO -> evd, mkvar evd inj e -let trans_expr env evd e = +let trans_expr dtyp env evd e = try - let evd, prf = trans_expr env evd e in + let evd, prf = trans_expr dtyp env evd e in evd, pp_trans_expr env evd e prf with Not_found -> raise @@ -1350,33 +1404,33 @@ let trans_un_prop op_constr op_iff p1 prf1 = ( EConstr.mkApp (op_constr, [|p1'|]) , EConstr.mkApp (op_iff, [|p1; p1'; prf|]) ) -let rec trans_prop env evd e = +let rec trans_prop dtyp env evd e = match classify_prop env evd e with | BINOP ({op_constr; op_iff}, p1, p2) -> - let evd, prf1 = trans_prop env evd p1 in - let evd, prf2 = trans_prop env evd p2 in + let evd, prf1 = trans_prop dtyp env evd p1 in + let evd, prf2 = trans_prop dtyp env evd p2 in evd, trans_bin_prop op_constr op_iff p1 prf1 p2 prf2 | UNOP ({op_constr; op_iff}, p1) -> - let evd, prf1 = trans_prop env evd p1 in + let evd, prf1 = trans_prop dtyp env evd p1 in evd, trans_un_prop op_constr op_iff p1 prf1 | OTHEROP (c, a) -> ( try let k, t = find_option - (match_operator env evd c a None) + (match_operator dtyp env evd c a None) (ConstrMap.find_all env evd c !table_cache) in let n = Array.length a in match k with | BinRel {decl = br; deriv = rop} -> let evd, a1 = - trans_expr env evd + trans_expr dtyp env evd { constr = a.(n - 2) ; typ = rop.EBinRelT.source ; inj = rop.EBinRelT.inj } in let evd, a2 = - trans_expr env evd + trans_expr dtyp env evd { constr = a.(n - 1) ; typ = rop.EBinRelT.source ; inj = rop.EBinRelT.inj } @@ -1385,9 +1439,9 @@ let rec trans_prop env evd e = | _ -> evd, IProof with Not_found | DestKO -> evd, IProof ) -let trans_check_prop env evd t = +let trans_check_prop dtyp env evd t = if is_prop env evd t then - let evd, p = trans_prop env evd t in + let evd, p = trans_prop dtyp env evd t in evd, Some p else evd, None @@ -1395,11 +1449,11 @@ let get_hyp_typ = function | NamedDecl.LocalDef (h, _, ty) | NamedDecl.LocalAssum (h, ty) -> (h.Context.binder_name, ty) -let trans_hyps env evd l = +let trans_hyps dtyp env evd l = List.fold_left (fun (evd, acc) decl -> let h, ty = get_hyp_typ decl in - match trans_check_prop env evd ty with + match trans_check_prop dtyp env evd ty with | evd, None -> evd, acc | evd, Some p' -> evd, (h, ty, p') :: acc) (evd, []) l @@ -1478,13 +1532,13 @@ let do_let tac (h : Constr.named_declaration) = ignore (let eq = eq() in find_option - (match_operator env evd eq + (match_operator (* eq ??? *) eq env evd eq [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|] None) (ConstrMap.find_all env evd eq !table_cache)); tac x (EConstr.of_constr t) (EConstr.of_constr ty) with Not_found -> Tacticals.tclIDTAC) -let iter_let_aux tac = +let iter_let_aux tac = Proofview.Goal.enter (fun gl -> let env = Proofview.Goal.env gl in let sign = Environ.named_context env in @@ -1509,17 +1563,17 @@ let iter_let (tac : Ltac_plugin.Tacarg.tacvalue) = let elim_let = iter_let_aux elim_binding -let zify_tac = + +let tify_op (ty:GlobRef.t) = Proofview.Goal.enter (fun gl -> Rocqlib.check_required_library ["Stdlib"; "micromega"; "ZifyClasses"]; - Rocqlib.check_required_library ["Stdlib"; "micromega"; "ZifyInst"]; init_cache (); let evd = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sign = EConstr.named_context env in - let concl = Proofview.Goal.concl gl in - let evd, concl = trans_check_prop env evd concl in - let evd, hyps = trans_hyps env evd sign in + let dtyp = EConstr.of_constr (UnivGen.constr_of_monomorphic_global env ty) in + let evd, concl = trans_check_prop dtyp env evd (Proofview.Goal.concl gl) in + let evd, hyps = trans_hyps dtyp env evd sign in let l = CstrTable.get () in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (tclTHENOpt concl trans_concl @@ -1528,6 +1582,8 @@ let zify_tac = (List.rev_map (fun (h, p, t) -> trans_hyp h p t) hyps)) (CstrTable.gen_cstr l)))) +let zify_op = fun () -> tify_op (Lazy.force rocq_Z) + type pscript = Set of Names.Id.t * EConstr.t | Pose of Names.Id.t * EConstr.t type spec_env = @@ -1633,8 +1689,7 @@ let find_hyp evd t l = let find_proof evd t l = if EConstr.eq_constr evd t (op_True()) then Some (op_I()) else - let l = List.map (fun decl -> NamedDecl.get_id decl, NamedDecl.get_type decl) l in - find_hyp evd t l + let l = List.map (fun decl -> NamedDecl.get_id decl, NamedDecl.get_type decl) l in find_hyp evd t l (** [sat_constr env evd sub taclist hyps c d]= (sub',taclist',hyps') where - sub' is a fresh subscript obtained from sub @@ -1684,8 +1739,8 @@ let saturate = init_cache (); let table = CstrTable.HConstr.create 20 in let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - let hyps = EConstr.named_context env in + let env = Proofview.Goal.env gl in + let hyps = EConstr.named_context env in let evd = Proofview.Goal.sigma gl in let rec sat t = match EConstr.kind evd t with diff --git a/src/zify.mli b/src/tify.mli similarity index 93% rename from src/zify.mli rename to src/tify.mli index c07fbd26b8..cb693da31f 100644 --- a/src/zify.mli +++ b/src/tify.mli @@ -26,7 +26,8 @@ module BinOpSpec : S module UnOpSpec : S module Saturate : S -val zify_tac : unit Proofview.tactic +val tify_op : Names.GlobRef.t -> unit Proofview.tactic +val zify_op : unit -> unit Proofview.tactic val saturate : unit Proofview.tactic val iter_specs : unit Proofview.tactic [%%if rocq = "9.0" || rocq = "9.1" || rocq = "9.2"] diff --git a/theories/Tify.v b/theories/Tify.v new file mode 100644 index 0000000000..f2c9485711 --- /dev/null +++ b/theories/Tify.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(*