GitHub - shingarov/MachineArithmetic: A mathematical foundation for Smalltalk-25 (original) (raw)
A mathematical foundation for Smalltalk-25
This repo contains the code for the theorem prover we describe in our papersTowards a Dynabook for verified VM constructionand Live Proof-by-Induction.
How to load
...into Pharo or GT
Metacello new
baseline: 'MachineArithmetic';
repository: 'github://shingarov/MachineArithmetic:pure-z3';
load.
To create fresh image for development
Either use shortcut:
git clone https://github.com/shingarov/MachineArithmetic
cd MachineArithmetic/pharo
make
./pharo MachineArithmetic.image
...or do it by hand:
- Clone the repository
git clone https://github.com/shingarov/MachineArithmetic - Download Pharo
# Be carefull, running a script downloaded from internet is not advisable!
curl https://get.pharo.org/64/80+vm | bash - Load code into Pharo image:
./pharo Pharo.image save MachineArithmetic
./pharo MachineArithmetic.image metacello install tonel://./MachineArithmetic/src BaselineOfMachineArithmetic
./pharo MachineArithmetic.image eval --save "(IceRepositoryCreator new location: 'MachineArithmetic' asFileReference; createRepository) register" ...into Smalltalk/X
NOTE: The following instructions assume you have a recent Smalltalk/X jv-branch, i.e., a version newer than 2021-12-09 (older versions might not have required Pharo compatibility support — Tonel, PackageManifests, ... — built in).
NOTE: Following instructions load only core MachineArithmetic package (basically Z3 bindings) as the rest is not supported on Smalltalk/X at the moment.
Either use shortcut:
git clone https://github.com/shingarov/MachineArithmetic
cd MachineArithmetic/stx
make
make run
...or do it by hand:
- Clone the repository:
git clone https://github.com/shingarov/MachineArithmetic.git - In Smalltalk/X, execute:
"/ Tell Smalltalk/X where to look for MachineArithmetic packages
Smalltalk packagePath add: '/where/you/cloned/it/MachineArithmetic'.
"/ Load MachineArithmetic
Smalltalk loadPackage: 'BaselineOfMachineArithmetic'.