Jason Gross
Jason Gross
### `brew gist-logs ` link OR `brew config` AND `brew doctor` output ```shell % brew gist-logs agda Error: No logs. ``` ``` % brew config HOMEBREW_VERSION: 4.4.1 ORIGIN: https://github.com/Homebrew/brew HEAD:...
Not sure if I should be reporting this here or in https://github.com/ocaml/setup-ocaml/issues/866, so I've reported it in both places. opam config report (failing version 2.2.1) ``` # opam config report...
If compcert does not install `.v` and `.glob` files, the bug minimizer cannot minimize any bugs in projects that are built on top of compcert. Note that `coq_makefile`-made makefiles install...
This will allow https://github.com/coq/opam/tree/master/extra-dev/packages/coq-compcert/coq-compcert.dev to drop the patch that makes `./configure` compatible with unreleased / dev versions of menhir.
#### Description of the problem ```coq From Coq Require Import Uint63 List PArray. Open Scope uint63_scope. Open Scope list_scope. Check [| 1; 2 | 0 : int |]. Import ListNotations....
#### Description of the problem ``` $ cat foo.v ``` ```coq Require Import Coq.derive.Derive. Derive foo SuchThat (foo = 1) As foo_eq. Proof. subst foo; reflexivity. Qed. ``` ``` $...
The name & email used is on the left, please request changes / make a suggestion if you want a different email address to show up for `git shortlog -nse`....
conf-cc?
Would it be possible to add a conf- package for the presence of any C compiler addressable by `cc`, a la https://github.com/ocaml/opam-repository/blob/master/packages/conf-c%2B%2B/conf-c%2B%2B.1.0/opam ?
``` _bench/opam.NEW/log/coq-bedrock2-602151-478bfb.out ### output ### # [...] # > ^^^^^^^^^^ # Error: This number is too large. # # Coq < # Unnamed_thm < # Unnamed_thm < # Unnamed_thm <...