Chun Tian

Solaris x86 and x86_64 patches (tested on Solaris 10 and 11)

1

Currently the SBCL binaries provided on sbcl.org is for version 1.2.7, the binaries may work on Solaris 11 but cannot run on Solaris 10. I have successfully built latest SBCL...

Creating a conversion of indefinite integrals (antiderivatives) of real functions

2

Following some recent discussions on Slack, I'm considering writing a HOL conversion for computing indefinite integrals (antiderivatives) of real functions, which may be called `INTEGRATE_CONV`. After some investigations on the...

Fixed OpenTheory build issues (#1045) introduced in #1043

5

Hi, this PR fixes the OpenTheory build issues described in #1045, i.e. a lot of leaking assumptions when installing `hol-real`. As I mentioned in #1045, these issues were introduced when...

OpenTheory issues after moving some definitions and theorems into realaxTheory

4

Hi, I'm sorry to report that, the OpenTheory packages (in particular, `hol-real`) built after #1043 (the new `REAL_ARITH_TAC`) now have a lot of leaking assumptions not covered by OpenTheory base...

Changes in COND_ELIM_CONV and SUB_AND_COND_ELIM_CONV

6

Hi, I occasionally found that the outputs of two COND-elimination conversions `COND_ELIM_CONV` and `SUB_AND_COND_ELIM_CONV` have changed w.r.t. their documentation, for instance: ``` > COND_ELIM_CONV ``!f n. f (if (SUC n...

Remaining issues of HOL's OpenTheory packaging

2

Following PR #803, I found the following remaining issues in OpenTheory packaging: 1. The recently added `itself` type in `boolTheory` introduced some new type, constant and theorems. When these theorems...

Hi, I have my `HOL4_YICES_EXECUTABLE` environment variable set to Yices 1.0.40 since many years ago. I never actually use Yices to do anything: ``` $ echo $HOL4_YICES_EXECUTABLE /Users/binghe/ML/yices-1.0.40/bin/yices ``` Usually...

Command sequence for installing HOL's OpenTheory packages

3

Before building HOL with `--otknl`, the `opentheory` command must be available and initialized (shell command: `opentheory init`), and the OT package "base-1.221" [1] must be already installed (shell command: `opentheory...

Hi, Currently all Axiom commands are repeated after hitting enter, e.g. below is some usage of August 2014 binary release: ``` This function is obsolete -- use SET-STARTING-HOLE-DIVISOR instead AXIOM...

In `src/Makefile.pamphlet`, the following chunk of code extracts another `Makefile` from `bookvol6.pamphlet` into `src/sman` and execute the new Makefile for building some executions (`spadclient`, `session`, etc.): ``` \begin{chunk}{smandir} smandir: ${SPD}/books/bookvol6.pamphlet...