Skip to content

Instantly share code, notes, and snippets.

Avatar

Paolo G. Giarrusso Blaisorblade

View GitHub Profile
View log.txt
```
$ git rev-parse HEAD
e31304d4d76d616130bc635457f12d5a6878b3d8
$ dune test --display verbose test/blackbox-tests/test-cases/promote/
Shared cache: enabled
Workspace root: /Users/pgiarrusso1/git-bedrock/dune
Running[0]: /Users/pgiarrusso1/git-bedrock/dune/_opam/bin/ocamlc.opt -config > /var/folders/6q/2ycxnczj1qsgwsk7lg3yd4bh0000gn/T/dune_f0778e_output
Dune context:
{ name = "default"
; kind = "default"
@Blaisorblade
Blaisorblade / leaky_strings.v
Last active Jul 19, 2022
Coq strings are so logical, they're literally built on truth
View leaky_strings.v
Require Import iris.proofmode.proofmode.
Lemma string_fun (PROP : bi) (X : PROP) : X ⊢ X.
Proof.
iIntros "X".
generalize true; intros.
Show.
(*
1 goal
@Blaisorblade
Blaisorblade / finite.v
Created May 19, 2022
bedrock.prelude.finite
View finite.v
(*
* Copyright (c) 2021 BedRock Systems, Inc.
*
* This software is distributed under the terms of the BedRock Open-Source License.
* See the LICENSE-BedRock file in the repository root for details.
*)
From stdpp Require Export finite.
From bedrock.prelude Require Import base bool numbers list_numbers gmap list fin_sets.
@Blaisorblade
Blaisorblade / elpi-5488-6af0b5.out
Created Mar 27, 2022
Elpi 1.14.3 vs OCaml 4.14.0 trunk — compile errors
View elpi-5488-6af0b5.out
dune build -p elpi -j 11 @all
(cd _build/default && /Users/pgiarrusso1/.opam/4.14.0+trunk/bin/ocamlc.opt -linkall -g -bin-annot -I src/.elpi.objs/byte -I src/.elpi.objs/public_cmi -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/camlp5 -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/ppx_deriving/runtime -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/re -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/re/str -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/result -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/seq -I /Users/pgiarrusso1/.opam/4.14.0+trunk/lib/stdlib-shims -I trace/runtime/.trace_ppx_runtime.objs/byte -no-alias-deps -open Elpi__ -o src/.elpi.objs/byte/elpi__Parser.cmi -c -intf src/parser.pp.mli)
File "src/parser.mli", line 34, characters 89-102:
34 | val parse_program_from_stream : parser_state -> print_accumulated_files:bool -> Loc.t -> char Stream.t -> Program.t
^^^^^^^^^^^^^
Alert deprecated: module Stdlib.Stream
Use th
View decide_True_broke.v
(* Coq 8.15.0, Iris dev.2022-01-24.0.72a4bd62. *)
From iris.prelude Require Import prelude.
Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
Succeed by rewrite ->decide_True.
Fail rewrite decide_True.
Fail rewrite (decide_True (A := nat) _ 0).
Fail rewrite (@decide_True nat (@eq nat 0 0) _ _ _ _).
@Blaisorblade
Blaisorblade / hide_global_hints.v
Created Feb 26, 2022
Coq: Opaque module ascription already hides global hints
View hide_global_hints.v
Require Import stdpp.base.
Module Type FOO.
Definition number : Set := nat.
End FOO.
Module Import foo : FOO.
Definition number : Set := nat.
Fail #[global] Instance number_inh : Inhabited number := _.
@Blaisorblade
Blaisorblade / modules_instances.v
Last active Jan 31, 2022
Demonstrate how opaque ascription takes hints from the interface, while transparent ascription takes them from bodies
View modules_instances.v
Require Import stdpp.base.
Require Import NArith.
(* We omit [Require Import stdpp.numbers.], which already has the [Inhabited]
instances we test here. *)
Module Type X.
#[global] Instance a : Inhabited nat.
Proof.
Fail apply _.
View TermEquality_universes.v
(* Distributed under the terms of the MIT license. *)
From Coq Require Import CMorphisms.
From MetaCoq.Template Require Import config utils Reflect Ast AstUtils Induction LiftSubst Reflect.
Require Import ssreflect.
From Equations.Prop Require Import DepElim.
Set Equations With UIP.
Definition R_universe_instance R :=
fun u u' => Forall2 R (List.map Universe.make u) (List.map Universe.make u').
@Blaisorblade
Blaisorblade / dune
Last active Nov 27, 2021
Evidence for https://github.com/coq/coq/issues/15255; build by clone + dune build
View dune
(coq.theory
(name notation_test)
(flags (:standard)))
View opaque-opaque.v
From Coq Require Import Vector.
Lemma foo : nat.
Proof. exact 1. Qed.
Eval compute in foo.
Eval vm_compute in foo.
Lemma bar : nat.
Proof. exact 1. Defined.