- 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 asP(actual|predicted)
. - Simlarly, we define recall as the fraction of
A
that was correctly predicted:$|P \cap A|/|A|$ . Probabilistically, this isP(predicted|actual)
.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(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. | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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}> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; 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)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;;;; -*- 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: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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% |
- 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.
The compiler panics with the error:
NewerOlder