HimML  Download Page

HimML on the Mac: for Mac OS X 10.15 and higher.

The HimML documentation is online!
(Beware though of slight inaccuracies: I've noticed to my great disappointment that conditional compilation was not working; anyway it is obsolescent; however, and after six years, the debugger is finally working!)
(Last minute note: do not use bison 1.35 for compiling HimML, as it bugs on HimML's grammar file; other versions of bison I know do work.)

HimML (HimML Is a Map-oriented  ML) is an extension of core Standard ML with primitive finite set and map datatypes, all sorts of comprehensions and quantifications over sets, maps and lists.  It is a rather comfortable language to code theorem provers or symbolic computation programs in. It was implemented by Jean Goubault-Larrecq while he was at Bull S.A., then at GIE Dyade, then at LSV, ENS Cachan. It is licensed under GPL, see files COPYRIGHT and COPYING.

The HimML implementation contains a bytecode compiler and interpreter, with a primitive module mechanism.  It can be used through a toplevel (himml) or as a compiler (himml -c). Current version is alpha 18, revision 3, dated December 11, 2008. Documentation is included in the Doc/refman.dvi file of the distribution.

HimML is available on Unix machines (and Amigas): see below; and on MacOSX: see above (Just click and follow instructions).

The current source distribution is here. (If you clicked and got garbage on your screen, come back to this page and click this link while holding the shift key down.)
(For XEmacs support, please use the emacs-mode.elc and emacs-site.el files (see below): sorry, the above sources should only work on modern GNU Emacsen.)

Uncompress with unzip. This creates a directory Alpha19 containing all sources. Go to Alpha19, look at the OPTIONS file if you wish to change any parameters, type ./makemake, then make, then make install. Docs are in Alpha19/Doc.

 On Linux >=2.0.30 with libc6 (type ls -al /lib/libc.so*: if you get a file named libc.so.6, you've got libc6), you may instead want to get the binaries directly (although the following are now a bit ancient):
 

The HimML toplevel and bytecode compiler (himml)
The HimML bytecode interpreter (himmlrun)
The HimML dependency generator (himmldep)
The HimML linker and library archiver (himmllnk)
The HimML package creator, used by himmllnk (himmlpack)
The HimML native code compiler (prototype version, ultra-pessimizing) (himmlx); usage: himmlx bytecode-file. Requires gcc, installing the library libhimml.a somewhere in you lib path (typically /usr/local/lib), and the include file himmlx.h somewhere in your include path (typically /usr/local/include).

Put them into /usr/local/bin (don't forget to call chmod a+x on them first!). You may also want to get the Emacs mode files:
 

The compiled HimML mode file (himml-mode.elc)

The source of the HimML mode file (himml-mode.el)
The HimML mode entry file (himml-site.el)

Put them in your Emacs Lisp directory, typically /usr/share/emacs/site-lisp/, and add the following line to your .emacs file:

(load "himml-site")

This direct installation procedure is not recommended, as it violates the copyright associated with HimML, and also fails to copy the COPYING and COPYRIGHT files that contain copyright information for HimML.

Version 16: The main new feature compared with HimML alpha 15 is support for lexical scanners and parsers generated by tools derived from flex and bison. These tools are hlex, a lexical scanner generator, and hyacc, a parser generator. For each, the compressed archive contains a directory (Hlex/, resp. Hyacc/) containing all sources, docs and copyright information. To compile, enter the relevant directory, type ./configure, then make, then make install.

The binaries for Linux >=2.0.30, libc6, are here for hlex and here for hyacc.

After getting them, call chmod a+x on them, then install them in /usr/local/bin.

The man pages for hlex and for hyacc.

Again, this direct installation procedure is not recommended, as it violates the copyright associated with hlex and hyacc, and also fails to copy the COPYING files that contain copyright information for these tools.

Another new feature in HimML alpha 16 is support for big integer and big modular integer arithmetic, based on code by Arjen Lenstra. See the docs for details.

Happy hacking!