script.lisp
primitives.lisp
primitive-lemmas.lisp
keytuples.lisp
m5.lisp
m5-lemmas.lisp
m5-fact.lisp
m5-fib.lisp
m5-magic.lisp
Copy these files to your space. I recommend creating a new subdirectory of your space, called m5/ upon which to store your M5 work. Then connect to that directory and start ACL2. Then execute
(ld "script.lisp" :ld-pre-eval-print t)That will recertify all the books and take several minutes, perhaps as long as 5 or 10 depending on your machine.
You should then be able to start a fresh ACL2 and type:
(include-book "m5") (in-package "M5")to experiment with M5.
More files may be added as time goes by.