Skip to content

Instantly share code, notes, and snippets.

View bollu's full-sized avatar

Siddharth bollu

View GitHub Profile
@bollu
bollu / lean-runtime-stats-on
Created March 26, 2024 22:22
cmake -DRUNTIME_STATS=ON
make -j stage1
/homes/sb2743/temp/lean4/src/runtime/allocprof.cpp: In constructor ‘lean::allocprof::allocprof(std::ostream&, const char*)’:
/homes/sb2743/temp/lean4/src/runtime/allocprof.cpp:12:25: error: ‘g_num_ctor’ was not declared in this scope; did you mean ‘m_num_ctor’?
12 | m_num_ctor = g_num_ctor;
| ^~~~~~~~~~
| m_num_ctor
/homes/sb2743/temp/lean4/src/runtime/allocprof.cpp:13:25: error: ‘g_num_closure’ was not declared in this scope; did you mean ‘m_num_closure’?
13 | m_num_closure = g_num_closure;
| ^~~~~~~~~~~~~
| m_num_closure

Precision, Recall, and all that.

  • Setting: we have some theorem goal $g$, a dataset of mathematical lemmas $D$, a set of actually useful lemmas $A$, and a set of predicted lemmas $P$.
  • We want to provide a good measure of how "good" $P$ is with respect to the ground truth $A$.
  • We begin by defining precision, which is the fraction of $P$ that was correct: $|P \cap A|/|P|$. Probabilistically, this can be seen as P(actual|predicted).
  • Simlarly, we define recall as the fraction of A that was correctly predicted: $|P \cap A|/|A|$. Probabilistically, this is P(predicted|actual).
@bollu
bollu / let-star-terrible-compiler-error.lisp
Created January 10, 2022 18:00
Why does SBCL not warn that the let* makes no SYNTACTIC sense?
(defgeneric errormsg (x))
(let* (x (errormsg nil)) x)
;; [slime-compile-defun]
;; cd c:/Users/bollu/quicklisp/local-projects/hoopl/src/hoopl/
;; 1 compiler notes:
;;
;; hoopl.lisp:244:1:
;; style-warning: The variable ERRORMSG is defined but never used.
@bollu
bollu / error
Created January 8, 2022 14:35
c2mop usage does not compile correctly
hoopl.lisp:175:56:
read-error:
READ error during COMPILE-FILE:
Package C2MOP does not exist.
Line: 175, Column: 56, File-Position: 5631
Stream: #<SB-INT:FORM-TRACKING-STREAM for "file c:\\Users\\bollu\\phd\\mlir-hoopl-rete\\src\\hoopl\\hoopl.lisp" {25891499}>
@bollu
bollu / common-lisp-backtrace
Created January 7, 2022 15:21
Learning how to use the SBCL+sly debugger
0: ("undefined function" #<STANDARD-CLASS COMMON-LISP-USER::INST-ADD>)
1: ((:METHOD DEEPEQ (T T)) #<INST-ADD {1001E94723}> #<INST-ADD {1001E947A3}>) [fast-method]
2: (SB-INT:SIMPLE-EVAL-IN-LEXENV (DEEPEQ (MK-INST-ADD :X :Y 1) (MK-INST-ADD :X :Y 1)) #<NULL-LEXENV>)
3: (SB-INT:SIMPLE-EVAL-IN-LEXENV (ASSERT-EQUAL (DEEPEQ (MK-INST-ADD :X :Y 1) (MK-INST-ADD :X :Y 1)) T) #<NULL-LEXENV>)
4: (EVAL (ASSERT-EQUAL (DEEPEQ (MK-INST-ADD :X :Y 1) (MK-INST-ADD :X :Y 1)) T))
5: (SLYNK::EVAL-REGION ";;;; -*- Mode: Common-Lisp; Author: Siddharth Bhat -*- ..)
6: ((LAMBDA NIL :IN SLYNK:INTERACTIVE-EVAL-REGION))
7: (SLYNK::CALL-WITH-RETRY-RESTART "Retry SLY interactive evaluation request." #<FUNCTION (LAMBDA NIL :IN SLYNK:INTERACTIVE-EVAL-REGION) {10015A3F$ 8: (SLYNK::CALL-WITH-BUFFER-SYNTAX NIL NIL #<FUNCTION (LAMBDA NIL :IN SLYNK:INTERACTIVE-EVAL-REGION) {10015A3F4B}>)
9: (SB-INT:SIMPLE-EVAL-IN-LEXENV (SLYNK:INTERACTIVE-EVAL-REGION ";;;; -*- Mode: Common-Lisp; Author: Siddharth Bhat -*- ..)
10: (EVAL (SLYNK:INTERACTIVE
;; equivalent upto structure
(defgeneric deepeq (x y))
(defmethod deepeq ((x number) y)
(equal x y))
(defmethod deepeq ((x symbol) y)
(equal x y))
(defmethod deepeq (x y)
;; quoted initarg
(defclass foo ()
((foo-field :initarg foo-initarg :accessor foo-accessor)))
(defparameter *foo* (make-instance 'foo 'foo-initarg 10))
;; symbold initarg
(defclass bar ()
((bar-field :initarg :bar-initarg :accessor bar-accessor)))
(defparameter *bar* (make-instance 'bar :bar-initarg 10))
@bollu
bollu / hoopl-clos.lisp
Last active January 6, 2022 04:56
Partial hoopl implementation in common lisp, put up for critique
;;;; -*- Mode: Common-Lisp; Author: Siddharth Bhat -*-
;;;; https://google.github.io/styleguide/lispguide.xml
;;;; https://jtra.cz/stuff/lisp/sclr/index.html
;;;; https://lispcookbook.github.io/cl-cookbook/data-structures.html
;;;; https://github.com/bollu/mlir-hoopl-rete/blob/master/reading/hoopl-proof-lerner.pdf
;;;; https://learnxinyminutes.com/docs/common-lisp/
;;;; https://lispcookbook.github.io/cl-cookbook/clos.html
;;;; https://malisper.me/debugging-lisp-part-1-recompilation/
;;; errors and restarts:
Report for stdlib
stdlib [0] ( 2 single benchmarks)
wall-clock mean = 241.(113), deviation = 10.59262%
stdlib [1] ( 2 single benchmarks)
wall-clock mean = 211.(160), deviation = 20.19648%
Equal program blocks
stdlib [0] ⟷ stdlib [1]
wall-clock confidence = 61%, speed up = 12.42%
@bollu
bollu / issue.md
Last active October 4, 2021 15:41
PANIC at Lean.Expr.bindingDomain! Lean.Expr:618:23: binding expected

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

The compiler panics with the error: