Commits on Jun 25, 2017
Commits on Jun 23, 2017
  1. Make by and suffices_by report failing tactics with line number

    Include test cases
    mn200 committed Jun 23, 2017
  2. Improve locn data coming out of low-level lexing

    In particular, the locn associated with the AQ token coming out of
    `^t` would never include a good <line number>-<column number> pair.
    mn200 committed Jun 22, 2017
  3. Remove float_negate1985 and float_abs1985

    This seems to have been half done in
    xrchz committed Jun 23, 2017
Commits on Jun 22, 2017
  1. Minor changes within floating-point theory.

    • The operations float_negate1985 and float_abs1985 have been removed.
    • Added a predicate float_is_signalling and renamed float_some_nan to float_some_qnan.
    • Fixed problem with EQ_tm and GT_tm being swapped in binary_ieeeSyntax.
    acjf3 committed Jun 22, 2017
Commits on Jun 21, 2017
  1. Merge in branch 'master'

    mn200 committed Jun 21, 2017
  2. Use git clean in regression build to get rid of more stuff

    build cleanAll is all very well, but it may miss things, and I do want
    to test the build from a clean state.
    mn200 committed Jun 21, 2017
  3. Get holfoot executables to build given change to quotation filter

    Not clear to me if these holfoot executables are tested once built,
    but they do now at least build.
    mn200 committed Jun 19, 2017
Commits on Jun 19, 2017
  1. Another fix for the new "by".

    acjf3 committed Jun 19, 2017
  2. Add arm_stepLib tool support for some SUBS PC instructions.

    These instructions are used for exception return.
    acjf3 committed Jun 19, 2017
Commits on Jun 15, 2017
Commits on Jun 14, 2017
  1. Remove an unnecessary line in the file

    The use of the "built-in" mlton mlb only needs to be done in, where Systeml.sml is referenced, requiring a pointer
    equality implementation.
    mn200 committed Jun 14, 2017
  2. hol-mode: fix copy-region-as-hol-definition-quietly

    In commit d3c3a92 the prefix argument
    of copy-region-as-hol-definition-quietly. This is very sensible, but
    afterwards copy-region-as-hol-definition-quietly could not be used
    interactively any more, since the interactive code was not adapted. This
    commit fixes it.
    Thomas Tuerk committed Jun 14, 2017
  3. add test case for issue 416

    Thomas Tuerk committed Jun 14, 2017
  4. Git-ignore a build file in tools

    This might be generated by the mlton build
    mn200 committed Jun 14, 2017
  5. MLton implementation of build

    Compile with mlton in the tools directory and then mv/cp the
    resulting executable into the HOL/bin directory.
    mn200 committed Jun 14, 2017
Commits on Jun 13, 2017
  1. fix issue #416

    Thomas Tuerk committed Jun 13, 2017
  2. Make script failures actually cause Holmake failures

    The shell-script needs a
        set -e
    line at the top to stop poly failures from being ignored.
    mn200 committed Jun 13, 2017
Commits on Jun 12, 2017
  1. Give more diagnostic output in shell-script that builds thy scripts

    This is not unhelpful in itself but is more of an experiment to try
    and diagnose the issues Ramana is having.
    mn200 committed Jun 12, 2017
Commits on Jun 9, 2017
  1. Add theorem: weaken the comparison in SORTED for a distinct list

    This is useful to move from a total order ($<=), which most of the
    verified sorting algorithms require, to a strict order ($<).
    xrchz committed Jun 9, 2017
  2. Fix Vim mode's suffices_by

    Since suffices_by now requires the tactic to succeed, use qsuff_tac
    instead to set up the goal interactively.
    xrchz committed Jun 9, 2017
Commits on Jun 8, 2017
Commits on Jun 7, 2017
  1. Make use of OS.IO.poll more robust

    Rather than comparing the polldesc type, compare the underlying
    iodesc. It appears that the pds returned from OS.IO.poll under mlton
    on Linux may not be the same as those passed in, even though the
    underlying iodescs (file descriptors) will be the same.
    mn200 committed Jun 7, 2017