Yannick Forster
Yannick Forster
It seems like most of the CI time is spent on building the dependencies. Is there a way to tell the CI to cache the files for e.g. CompCert in...
As just found out in a debugging session with @dominik-kirst, the `${SED}` line in `update_plugin.sh` removes the letter `r` from `cRelationClasses.mli` instead of removing the carriage `\r` if when using...
``` Notation "⟦ u ⟧_ v" := (Universe.univ_val v u) (at level 0, format "⟦ u ⟧_ v", v ident) : univ_scope. ``` in `Template.Universes` is incompatible with notations in...
I'd like to turn this Export into an Import. Otherwise we're running into trouble in CertiCoq: utils export the monad notation globally, which clashes with the monad notation used in...
Pretty much what the title says. Is this intended? I'm always surprised by `make install` after a successful `make all` taking a lot longer than it should, because first `translations`...
``` coq From MetaCoq.Template Require Import All. Require Import List String. Import ListNotations. MetaCoq Run (tmUnquoteTyped nat ((tConstruct (mkInd (MPfile ["Wrong"], "nat") 0) 0 []))). ``` results in ``` Error:...
``` Definition inverts {X} {Y} (g : X -> Y) (f : Y -> X) := forall x, g (f x) = x. From Equations Require Import Equations. Definition inspect...
Currently, when I want to simplify a goal containing `f1` and `f2`, both defined using Equations, I have to type `simp f1 f2`. It would be great if there would...
The `Program` mode automatically makes the equations behind a match accessible in proofs: ```Coq Program Definition test (n : nat) : {n = 0} + {n 0} := match Nat.eqb...
Is it possible to disable the opam cache (i.e. step 3 of the action)? I have a workflow which caches several things on its own, amongst them `.opam`, and the...