Lean type-checker written in Scala.
License: Apache License 2.0
Lean is an interactive theorem prover based on dependent type theory. For additional trust, Lean can export the generated proofs so that they can be independently verified. Trepplein is a tool that can check these exported proofs.
Trepplein is written in Scala, and requires SBT to build.
sbt stage
./target/universal/stage/bin/trepplein .../export.out
I'm a complete scala novice so take this with a pinch of salt, but I wanted to post this incase it helps anyone else who couldn't build trepplein.
Running sbt stage gave me numerous errors which lead me to scala/bug#11247 following the suggestion there and removing inline flags then re-running the build worked.
diff --git a/build.sbt b/build.sbt
index d537e73..5d49ac3 100644
--- a/build.sbt
+++ b/build.sbt
@@ -14,7 +14,7 @@ libraryDependencies += "org.specs2" %% "specs2-core" % "4.2.0" % "test"
scalacOptions ++= {
if (!scalaVersion.value.startsWith("2.12.")) Seq()
- else Seq("-opt:l:inline", "-opt-inline-from:**", "-opt-warnings")
+ else Seq("-opt-warnings")
}Consider the following input (found by running AFL on a minimal testing harness):
9 #NS 0 u
2 #NS 0 eq
3 #NS 0 alpha
1 #UP 1
0 #ES 1
4 #NS 0 a
1 #EV 0
5 #NS 0 alpt
2 #EV 1
3 #ES 0
4 #EP #BD 5 2 3
5 #EP #BD 4 1 4
6 #EP #BI 3 0 5
6 #NS 2 refl
7 #EC 2 1
8 #EA 7 2
9 #EA 8 1
10 #EA 9 1
11 #EP #BD 4 1 10
12 #EP #BI 3 0 11
#IND 2 2 6 1 6 12 1
leanchecker rejects this with the output:
line 4: _Map_base::at
but trepplein accepts it with the output:
-- successfully checked 3 declarations
On zulip, @digama0 annotated the input like this
9 #NS 0 u = `u
2 #NS 0 eq = `eq
3 #NS 0 alpha = `alpha
1 #UP 1 = u1 (???)
0 #ES 1 = Sort u1
4 #NS 0 a = `a
1 #EV 0 = #0
5 #NS 0 alpt = `alpt
2 #EV 1 = #1
3 #ES 0 = Sort 0
4 #EP #BD 5 2 3 = Π (alpt : #1), Sort 0
5 #EP #BD 4 1 4 = Π (a : #0) (alpt : #0), Sort 0
6 #EP #BI 3 0 5 = Π {alpha : Sort u1} (a : alpha) (alpt : alpha), Sort 0
6 #NS 2 refl = `refl
7 #EC 2 1 = eq.{u1}
8 #EA 7 2 = eq.{u1} #1
9 #EA 8 1 = eq.{u1} #1 #0
10 #EA 9 1 = eq.{u1} #1 #0 #0
11 #EP #BD 4 1 10 = Π (a : #0), eq.{u1} #0 a a
12 #EP #BI 3 0 11 = Π {alpha : Sort u1} (a : alpha), eq.{u1} alpha a a
#IND 2 2 6 1 6 12 1 =
inductive {u1} eq {alpha : Sort u1} (a : alpha) : Π (alpt : alpha), Sort 0
| refl : Π {alpha : Sort u1} (a : alpha), eq.{u1} alpha a a
The problem is on line 4, which constructs a universe parameter referencing a non-existent name.
In my current understanding, it seems pretty clear that this is a bug in trepplein -- it ought to be rejecting this input, because it uses a malformed universe variable.
When running on the exported file for group.lean in sbt, I get a stack overflow, which (as running in console shows) is in defining the preEnv. A hack that worked once is to add .toVector to exported commands, i.e., modify to
val exportedCommands = TextExportParser.parseFile(opts.inputFile).toVectorbut crashes are random and may be some problem with my setup.
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.