collares

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

collares

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

collares

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 (¬_)

collares

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

collares

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

$  ../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

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

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

collares

‘#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 ℕ

collares

[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 })