Skip to content

Instantly share code, notes, and snippets.

View collares's full-sized avatar

Mauricio Collares collares

View GitHub Profile
@collares
collares / cell_store.py
Last active August 25, 2022 12:33
An implementation of Bill Gosper's hashlife algorithm
class Store(object):
LOG_MAX_UNIVERSE = 60
# This is arbitrary, but it simplifies get_empty below.
DEAD_HASH = 0
ALIVE_HASH = LOG_MAX_UNIVERSE + 1
class MacrocellData(object):
def __init__(self, quadrants, result):
self.quadrants = quadrants
module plfa.Minimized where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Function using (_∘_)
data _×_ (A B : Set) : Set where
⟨_,_⟩ : A → B → A × B
proj₁ : ∀ {A B : Set} → A × B → A
module plfa.Minimized where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open import Function using (_∘_)
open import Data.List using (List; []; _∷_)
open import Data.List.All using (All; []; _∷_)
open import Data.List.Any using (Any; here; there)
open import Data.List.Membership.Propositional using (_∈_)
open import Relation.Nullary using (¬_)
module plfa.Lists where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax)
renaming (_,_ to ⟨_,_⟩)
open import plfa.Isomorphism using (_≃_)
data List (A : Set) : Set where
[] : List A
ubuntu@instance-20211207-1713:~/source/omalloc$ cat config.log
This file contains any messages produced by compilers while
running configure, to aid debugging if configure makes a mistake.
It was created by omalloc configure 0.9.6, which was
generated by GNU Autoconf 2.71. Invocation command line was
$ ./configure --disable-option-checking --prefix=/home/ubuntu/nixpkgs/outputs/out --disable-static --with-ntl=/nix/store/6x0g54b5bc1rb0b771rhy6gvmyhv157d-ntl-11.4.4 --disable-pyobject-module --enable-doc-build --enable-gfanlib CC=gcc CXX=g++ --enable-omalloc OMALLOC_LIBS=/home/ubuntu/source/omalloc/libomalloc.la OMALLOC_INCLUDES=-I/home/ubuntu/source --with-Singular RESOURCES_LIBS=/home/ubuntu/source/resources/libsingular_resources.la 'RESOURCES_INCLUDES=-I/home/ubuntu/source ' FACTORY_LIBS=/home/ubuntu/source/factory/libfactory.la 'FACTORY_INCLUDES=-I/home/ubuntu/source -I/home/ubuntu/source/factory -I/home/ubuntu/source/factory/include' --cache-file=/dev/null --srcdir=.
## --------- ##
@collares
collares / zeroRadical.res
Created December 19, 2021 00:42
zeroRadical.example output with option(prot) enabled
$ ../Singular/Singular -teqr12345678 --no-rc
> option(prot);
STDIN 1> option(prot);
> LIB "assprimeszerodim.lib";
STDIN 2> LIB "assprimeszerodim.lib";
> ring R = 0, (x,y), dp;
STDIN 3> ring R = 0, (x,y), dp;
> ideal I = xy4-2xy2+x, x2-x, y4-2y2+1;
STDIN 4> ideal I = xy4-2xy2+x, x2-x, y4-2y2+1;
> zeroRadical(I);
@collares
collares / expr.lean
Last active January 2, 2022 13:17
print(e) for the crashing expression in remove_unnnecessary_casts
category_theory.limits.wide_pullback_shape.hom.rec.{succ v₂ v₁}
category_theory.limits.walking_pair.{v₁}
(fun (t_1 : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (t_2 : category_theory.limits.wide_pullback_shape.{v₁} category_theory.limits.walking_pair.{v₁}) (ᾰ : category_theory.limits.wide_pullback_shape.hom.{v₁} category_theory.limits.walking_pair.{v₁} t_1 t_2), ((eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} X t_1) -> (eq.{succ v₁} category_theory.limits.walking_cospan.{v₁} Z t_2) -> (heq.{succ v₁} (quiver.hom.{succ v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category_struct.to_quiver.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.category.to_category_struct.{v₁ v₁} category_theory.limits.walking_cospan.{v₁} (category_theory.limits.wide_pullback_shape.category.{v₁} category_theory.limits.walking_pair.{v₁}))) X Z) (category_theory.category_struct.comp.{v₁ v₁} category_theory.limits.walking_cospan.{v₁}
@collares
collares / stacktrace.txt
Created October 17, 2023 12:45
terminate called after throwing an instance of 'lean::interrupted'
Thread 5 "lean" received signal SIGABRT, Aborted.
[Switching to Thread 0x7f2566ffd6c0 (LWP 598642)]
__pthread_kill_implementation (threadid=<optimized out>, signo=signo@entry=6, no_tid=no_tid@entry=0) at pthread_kill.c:44
44 pthread_kill.c: No such file or directory.
(gdb) bt
#0 __pthread_kill_implementation (threadid=<optimized out>, signo=signo@entry=6, no_tid=no_tid@entry=0) at pthread_kill.c:44
#1 0x00007f25775c1af3 in __pthread_kill_internal (signo=6, threadid=<optimized out>) at pthread_kill.c:78
#2 0x00007f2577572c86 in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#3 0x00007f257755c8ba in __GI_abort () at abort.c:79
#4 0x00007f25772a9a89 in __gnu_cxx::__verbose_terminate_handler() [clone .cold] () from /nix/store/xq05361kqwzcdamcsxr4gzg8ksxrb8sg-gcc-12.3.0-lib/lib/libstdc++.so.6
‘#synth CharZero ℕ’: StrictOrderedSemiring.to_charZero
‘#synth CharZero ℕ’: [Elab.command] [0.047845s] #synth CharZero ℕ
[Meta.synthInstance] ✅ AddMonoidWithOne ℕ
[Meta.synthInstance] new goal AddMonoidWithOne ℕ
[Meta.synthInstance.instances] #[@AddCommMonoidWithOne.toAddMonoidWithOne, @AddGroupWithOne.toAddMonoidWithOne]
[Meta.synthInstance] ✅ apply @AddGroupWithOne.toAddMonoidWithOne to AddMonoidWithOne ℕ
[Meta.synthInstance.tryResolve] ✅ AddMonoidWithOne ℕ ≟ AddMonoidWithOne ℕ
[Meta.synthInstance] new goal AddGroupWithOne ℕ
[Meta.synthInstance.instances] #[@AddCommGroupWithOne.toAddGroupWithOne, @Ring.toAddGroupWithOne]
[Meta.synthInstance] ✅ apply @Ring.toAddGroupWithOne to AddGroupWithOne ℕ
This file has been truncated, but you can view the full file.
[Elab.command] [4.214561s] set_option trace.Meta.Tactic.simp true in
example (c k : ℕ) (hk : ∀ (b : ℕ), k * b = k * c → b = c) (b : ℕ) (h : S k * b = S k * c) : b = c :=
by
simp_all (config := { zeta := false, beta := false, eta := false, iota := false, proj := false, decide := false })
sorry
[Elab.command] [4.214447s] example (c k : ℕ) (hk : ∀ (b : ℕ), k * b = k * c → b = c) (b : ℕ) (h : S k * b = S k * c) :
b = c :=
by
simp_all (config :=
{ zeta := false, beta := false, eta := false, iota := false, proj := false, decide := false })