diff options
| -rw-r--r-- | .gitlab-ci.yml | 15 | ||||
| -rw-r--r-- | default.nix | 21 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 3 | ||||
| -rw-r--r-- | shell.nix | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/8004.v | 47 |
6 files changed, 86 insertions, 6 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 773a89a46..11614bc38 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -240,12 +240,25 @@ pkg:nix: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git stage: test variables: + # By default we use coq.cachix.org as an extra substituter but this can be overridden + EXTRA_SUBSTITUTERS: https://coq.cachix.org + EXTRA_PUBLIC_KEYS: coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI= + # The following variables should not be overridden GIT_STRATEGY: none + CACHIX_PUBLIC_KEY: cachix.cachix.org-1:eWNHQldwUO7G2VkjpnjDbWwy4KQ/HNxht7H4SSoMckM= + NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= + dependencies: [] # We don't need to download build artifacts before_script: [] # We don't want to use the shared 'before_script' script: + # Use current worktree as tmpdir to allow exporting artifacts in case of failure - export TMPDIR=$PWD - - nix-build "$CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz" -K + # Install Cachix as documented at https://github.com/cachix/cachix + - nix-env -if https://github.com/cachix/cachix/tarball/master --substituters https://cachix.cachix.org --trusted-public-keys "$CACHIX_PUBLIC_KEY" + # We build an expression rather than a direct URL to not be dependent on + # the URL location; we are forced to put the public key of cache.nixos.org + # because there is no --extra-trusted-public-key option. + - nix-build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}" -K --extra-substituters "$EXTRA_SUBSTITUTERS" --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS" | if [ ! -z "$CACHIX_SIGNING_KEY" ]; then cachix push coq; fi artifacts: name: "$CI_JOB_NAME.logs" when: on_failure diff --git a/default.nix b/default.nix index 1be274081..d9317bcca 100644 --- a/default.nix +++ b/default.nix @@ -30,6 +30,9 @@ , buildIde ? true , buildDoc ? true , doInstallCheck ? true +, shell ? false + # We don't use lib.inNixShell because that would also apply + # when in a nix-shell of some package depending on this one. }: with pkgs; @@ -58,13 +61,13 @@ stdenv.mkDerivation rec { optional (!versionAtLeast ocaml.version "4.07") ncurses ++ [ ocamlPackages.ounit rsync which ] ) - ++ optionals lib.inNixShell ( + ++ optionals shell ( [ jq curl git gnupg ] # Dependencies of the merging script ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools ); src = - if lib.inNixShell then null + if shell then null else with builtins; filterSource (path: _: @@ -86,4 +89,18 @@ stdenv.mkDerivation rec { installCheckTarget = [ "check" ]; + passthru = { inherit ocamlPackages; }; + + meta = { + description = "Coq proof assistant"; + longDescription = '' + Coq is a formal proof management system. It provides a formal language + to write mathematical definitions, executable algorithms and theorems + together with an environment for semi-interactive development of + machine-checked proofs. + ''; + homepage = http://coq.inria.fr; + license = licenses.lgpl21; + }; + } diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 660e29ca8..f24ab2bdd 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -293,7 +293,7 @@ open Vars let constr_flags () = { Pretyping.use_typeclasses = true; - Pretyping.solve_unification_constraints = true; + Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = false; Pretyping.expand_evars = true } diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7b7973224..e02b5ab95 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -85,6 +85,9 @@ val solve : ?with_end_tac:unit Proofview.tactic -> val by : unit Proofview.tactic -> bool +(** Option telling if unification heuristics should be used. *) +val use_unification_heuristics : unit -> bool + (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined existential variable of the current focused proof by [c] or raises a UserError if no proof is focused or if there is no such [n]th @@ -1,4 +1,4 @@ # Some developers don't want a pinned nix-shell by default. # If you want to use the pin nix-shell or a more sophisticated set of arguments: -# $ nix-shell default.nix -import ./default.nix { pkgs = import <nixpkgs> {}; } +# $ nix-shell default.nix --arg shell true +import ./default.nix { pkgs = import <nixpkgs> {}; shell = true; } diff --git a/test-suite/bugs/closed/8004.v b/test-suite/bugs/closed/8004.v new file mode 100644 index 000000000..818639997 --- /dev/null +++ b/test-suite/bugs/closed/8004.v @@ -0,0 +1,47 @@ +Require Export Coq.Program.Tactics Coq.Classes.SetoidTactics Coq.Classes.CMorphisms . + +Set Universe Polymorphism. + +Delimit Scope category_theory_scope with category_theory. +Open Scope category_theory_scope. + +Infix "∧" := prod (at level 80, right associativity) : category_theory_scope. + +Class Setoid A := { + equiv : crelation A; + setoid_equiv :> Equivalence equiv +}. + +Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope. + +Open Scope list_scope. + +Generalizable All Variables. + +Fixpoint list_equiv `{Setoid A} (xs ys : list A) : Type := + match xs, ys with + | nil, nil => True + | x :: xs, y :: ys => x ≈ y ∧ list_equiv xs ys + | _, _ => False + end. + +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. + +Program Instance list_equivalence `{Setoid A} : Equivalence list_equiv. +Next Obligation. + repeat intro. + induction x; simpl; split; auto. + reflexivity. +Qed. +Next Obligation. + repeat intro. + generalize dependent y. + induction x, y; simpl; intros; auto. + destruct X; split. + now symmetry. + intuition. +Qed. +Next Obligation. +admit. +Defined. |