The latest push extracts the functions from the algebra as preparation for COQ proofs. There is still work to be done to decorate the functions in domains and packages with their signatures which is the next thing to pursue.
All of these functions are collected into obj/sys/proofs/coq.v if the make command line includes COQ=coq, otherwise the extraction step is ignored. The coq.v file is pushed through coqtop to rerun any proofs. At the moment all of the functions are comments. Part of the game is to prove the most primitive functions first. This has two advantages. First, the proofs can be used during more complex proofs. Second, a lot of the primitive functions are just calls to the underlying lisp code. The underlying lisp code is being proven using ACL2 (also against auto-extracted code chunks) so there is a nice focus on a small set of primitives that benefit both the lisp- and spad-level code. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
