ManTa 3.1. Beta 4
The main improvements of this version are:
- New independent tools: mancomp (compiler), manrew (rewriting motor),
mantheo (theorem prover), m2c (C code generator)
- New ocaml code generator as an independent tool: m2ocaml
- Along with this version the ManTa Benchmark is included: manbench .
It is based on the NQTHM92 Benchmark.
- A new rewriting algorithm has been implemented
- Better test programs: They check the rewriting module, the theorem prover,
the prototype generator, the independent tools and the plain interface.
- More documentation is included with the sources distribution
- Formal description of the ManTa language
- Technical reference manual of the kernel API
- Draft of the user manual
- Draft of a tutorial
- More predefined ADTs: BOOL, NAT, Char, List, Queue, String and Stack
- Several bugs have been fixed:
- It checks strong local confluence
- Better unification algorithm
- Parser can recognize remarks
- Better typing
- When user loads a type it loads all the dependent types
- Better administration of symbols table
- Support for longer expressions in ADTs
- Better memory administration in inductive proofs
- Improvements in the development process
- New coding and documentation standards
- Better tools to generate makefiles, documentation and distributions
Sources and precompiled versions
There are precompiled versions for DOS/Windows machines: m31b4dos.zip
The sources are available under the GPL and they can be compiled
practically in any machine with GNU tools (gcc and make): dm31b4.tar.gz or dm31b4.zip
