bollu

local lazypath = vim.fn.stdpath("data") .. "/lazy/lazy.nvim"
if not (vim.uv or vim.loop).fs_stat(lazypath) then
  local lazyrepo = "https://github.com/folke/lazy.nvim.git"
  vim.fn.system({ "git", "clone", "--filter=blob:none", "--branch=stable", lazyrepo, lazypath })
end
vim.opt.rtp:prepend(lazypath)

-- Make sure to setup `mapleader` and `maplocalleader` before
-- loading lazy.nvim so that mappings are correct.
-- This is also a good place to setup other settings (vim.opt)

bollu

local lazypath = vim.fn.stdpath("data") .. "/lazy/lazy.nvim"
if not (vim.uv or vim.loop).fs_stat(lazypath) then
  local lazyrepo = "https://github.com/folke/lazy.nvim.git"
  vim.fn.system({ "git", "clone", "--filter=blob:none", "--branch=stable", lazyrepo, lazypath })
end
vim.opt.rtp:prepend(lazypath)

-- Make sure to setup `mapleader` and `maplocalleader` before
-- loading lazy.nvim so that mappings are correct.
-- This is also a good place to setup other settings (vim.opt)

bollu

Lean (version 4.8.0, commit 1f4dea858243, Release)
Lean (version 4.8.0, commit 5281a01ae3a9, Release)

bollu

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

bollu

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

(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

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

 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

bollu

;; 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)

bollu

;; 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))