This is the repository for metamath-lamp (Lite Assistant for Metamath Proofs). Metamath-lamp is a proof assistant for creating formal mathematical proofs in the Metamath system. Unlike most other Metamath proof systems (such as mmj2 or original metamath-exe), users can use this proof assistant without installing anything; you can simply run it directly using your web browser. It's written in ReScript (a robustly typed programming language that compiles to JavaScript) using the React user interface library and Material UI Components. It's licensed under the MIT license.
You can use this proof assistant now by going to the Metamath-lamp web site.
For more information, see the Metamath-lamp Guide.
Here's a short video demo (without sound).
Here's a simple screenshot of metamath-lamp in action.
How to run locally:
git clone https://github.com/expln/metamath-lamp.git
cd metamath-lamp
npm install
npm run compile-with-deps
npx webpack --config webworker.webpack.config.js
Windows: copy /B /Y ".\dist\webworker-main.js" ".\public"
Mac/Linux: cp ./dist/webworker-main.js ./public
npm run start
How to run all unit tests
npm run compile-test-all-unit
How to run all integration tests
npm run compile-test-all-int
How to run a particular test
replace: "compile-test-single": "rescript && mocha --timeout 10000000 -g \"'put_test_name_here'\" src/**/test/**/*.js",
with: "compile-test-single": "rescript && mocha --timeout 10000000 -g \"'finds proofs for simple wffs'\" src/**/test/**/*.js",
npm run compile-test-single
How to debug
There is no standard way to debug ReScript code. But ReScript gets compiled to readable JS code. So it is possible to debug JS code. In order to debug any use case:
npm run compile