The purpose of this repository is to build a version of the Twelf logical framework that can be run in the "Classic Mac" environment of approximately System 7 era. The current emulation target is a Quadra 800 running System 7.5.3.
Status:
- ✅ Twelf runs and can typecheck simple signatures that are typed in by hand
- ✅ Application and document icons exist
- ✅ File IO (Open, Save) is implemented
- ✅ Scrolling of the input document works
- ✅ Selection of output text works
- ✅ Copy/Paste is implemented
- 🚫 Revert doesn't work yet
- 🚫 Unsafe Eval doesn't work yet
Much thanks to agoode for explaining a lot of this.
I'm using Retro68 to compile C to run on an emulated mac. I build qemu 8.2.2 from source with
sudo apt install libglib2.0-dev libpixman-1-dev libgtk-3-dev libasound2-dev libslirp-dev
mkdir build
cd build
../configure --target-list=m68k-softmmu --enable-gtk --enable-pixman --enable-slirp
make
I needed to put in this directory:
MacOS7.5.3.imgcreated byqemu-img create -f raw -o size=2G MacOS7.5.3.imgMacOS7.5.3.isofrom https://winworldpc.com/download/3dc3aec3-b125-18c3-9a11-c3a4e284a2efpram-macos.imgcreated byqemu-img create -f raw pram-macos.img 256bQuadra800.romfrom https://archive.org/details/mac_rom_archive_-_as_of_8-19-2011 andmv 'F1ACAD13 - Quadra 610,650,maybe 800.ROM' Quadra800.romSaved.hdacreated by going to https://infinitemac.org/1996/System%207.5.3 and moving some files (like netscape navigator and stuffit expander) toSaved HDand then mousing over the grey "Home" next to the apple icon, choosing "Settings" and doing "Save Disk Image" as.hda
On linux cross-compile host:
cd docker
make Twelf.binOn linux cross-compile host:
make serve # spawns a local web serverStart MacOS guest with ./qemu-macos. Inside MacOS guest:
- Launch Netscape Navigator from
Saved HD. - Go to
http://10.0.2.2:8000/(this is the host-local web server) - Download
Twelf.bin - Expand it in Stuffit Expander to create app named
Twelf.