Permalink
Commits on Apr 26, 2017
Commits on Apr 25, 2017
  1. Add some more floating-point theorems.

    Now covers square root and fused multiply add/sub.
    acjf3 committed Apr 25, 2017
Commits on Apr 24, 2017
  1. hol-mode: add hol-print-info

    I recently have the problem on various machines, that have multiple
    copies of HOL installed, to figure out which version is started by hol-
    mode. I did this by looking at the value of HOLDIR, the current load
    paths etc in ML and the used hol and holmake executables in Lisp. To
    simplify this process of looking up these values, this commit adds this
    functionality to hol-mode.
    thtuerk committed Apr 24, 2017
Commits on Apr 21, 2017
  1. Make mkmunge aware of holpaths

    Thanks to Yong Kiam for the bug report. Test case included.
    mn200 committed Apr 21, 2017
Commits on Apr 20, 2017
  1. Fix Holmake under Moscow ML

    I changed the API (to pass the function to "shell out" to) under
    Poly/ML but forgot to adjust the Moscow ML version.
    mn200 committed Apr 20, 2017
  2. Add test case for multi-directory holpath builds with a heap

    Attempting a small-scale recreation of the CakeML bug that Yong Kiam
    reported.
    mn200 committed Apr 20, 2017
  3. Make buildheap aware of relocation/.holpath variables

    Thanks to Yong Kiam for the bug report
    mn200 committed Apr 20, 2017
Commits on Apr 19, 2017
  1. Update MIPS model to include Mike Roe’s floating-point specification.

    Also improve treatment of memory operations (so as to be more similar to the CHERI model).
    acjf3 committed Apr 19, 2017
  2. Update for latest version of L3.

    acjf3 committed Apr 19, 2017
  3. Read .holpath directories to allow relocatable developments

    If there is a .holpath file in a directory containing a string with a
    name for the development under that directory, then the object
    files (.uo and .ui) in that directory will be easily relocatable
    because they won't use absolute paths, but will instead use
    $(devname)/ type paths.
    
    Multiple developments can combine in this way, and there is additional
    machinery to make sure that all of the relevant directories are
    scanned before reading and writing of object files happens.
    mn200 committed Apr 19, 2017
  4. Complete relocation-build feature

    Closes #105
    
    To be explicit, after building HOL in one directory one can then
    
    $ bin/build cleanForReloc
    $ cd ..
    $ mv HOL somewhere_else
    $ cd somewhere_else
    $ poly < tools/smart-configure.sml
    $ bin/build --relocbuild
    
    The last step (the "relocation" build) takes less than a minute and
    results in a functional system that is housed in a different location.
    
    Next step on this branch of work is to provide tools allowing other
    developments (those not under HOLDIR) to be moved in a similar way.
    mn200 committed Apr 19, 2017
Commits on Apr 18, 2017
  1. Make j1 Poly build pass on environment variable to sub-shells

    Also rename reloc_build to relocbuild internally (making SML variable
    name match command-line option name).
    mn200 committed Apr 18, 2017
Commits on Apr 14, 2017
Commits on Apr 13, 2017
  1. Write and read .uo/.ui files using the $(HOLDIR) variable

    This should make HOL installations portable (once heaps are rebuilt).
    mn200 committed Apr 13, 2017
  2. Let .uo and .ui files have $(envvar) prefixes in their paths

    This will let these files specify positions for source code that is
    independent of an absolute position in the file-tree hierarchy, but is
    relative to a fixed base. The first step is to allow $(HOLDIR) so that
    HOL can have its own .uo files be easily relocatable.
    
    Next step is to write .uo and .ui files using this facility.
    mn200 committed Apr 13, 2017
Commits on Apr 12, 2017
  1. provide first version of BackchainingLib

    This lib is used to combine matching preconditions against assumptions
    in the goalstack with conditional rewriting. This enables efficient
    backwards-chaining with theorems like
    
    ``!x y. R x y ==> !x' y'. complicated condition ==> R x' y'``
    thtuerk committed Apr 10, 2017
Commits on Apr 11, 2017
  1. VFP instruction parsing/printing improvements for ARMv7 model.

    Fix for VMRS when destination is APSR_nzcv.
    acjf3 committed Apr 11, 2017
  2. Update RISC-V SML code.

    Should have been included with commit 4b08982.
    acjf3 committed Apr 11, 2017
Commits on Apr 9, 2017
  1. tactictoe: minimization

    Thibault Gauthier committed Apr 9, 2017
  2. tactictoe: nice quotes

    Thibault Gauthier committed Apr 9, 2017
Commits on Apr 8, 2017
  1. tactictoe: prettyfier

    Thibault Gauthier committed Apr 8, 2017
  2. TacticToe: update

    Merge branch 'master' of git://github.com/HOL-Theorem-Prover/HOL
    Thibault Gauthier committed Apr 8, 2017
  3. tacticoe: removing unit

    Thibault Gauthier committed Apr 8, 2017
Commits on Apr 7, 2017
  1. Fix quotes in the HOL4/emacs interaction guide

    HOL4 was not recognising Latex curly quotes, so I changed them into
    the usual quotes. One can now just copy paste the code into emacs.
    
    I also fixed a typo in the proof of LESS_EQ_MULT.
    rmonat committed with xrchz Apr 7, 2017