HOL

HOL copied to clipboard

Warn if modules / theories only differ by case

1

This leads to very strange errors on case-insensitive file systems. Also arises if a theory is referenced in one place with one capitalisation and in another with a different one.

mn200

*Viz:* > SIMP_CONV (srw_ss() ++ numSimps.ARITH_ss) [] ``n2 + (fxx - 1) + 1 - n2``; Exception- UNCHANGED raised The `n2`'s should be cancelled even though the `-1` can't be...

mn200

Implement include directive for Holmakefiles

3

As per [GNU make's facility](https://www.gnu.org/software/make/manual/html_node/Include.html). The ability to go back and attempt to build include files that are not found might be an optional part of this feature. Currently, I'm...

mn200

Merge dprot and protect

5

There are two `Holmakefile` functions that, from a user's perspective, serve the same purpose: namely, protect strings that contain spaces or other unusual characters from being split into multiple items...

xrchz

I have found myself in a situation where thinking about operator precedence, while getting familiar with a new theory confuses me. It would be nice to have a set_trace option...

formrre

Holmakefile INCLUDES cleaner

1

I propose a mode for `Holmake` to detect and warn about redundant `INCLUDES`, i.e., directories that are included but for which no dependencies are found for any targets in the...

xrchz

compsets should become functional

1

The references hidden inside compsets make manipulating them a pain. They also make concurrent operation hard.

mn200

Better syntax for chained updates to functions and finite maps

2

Chained updates look bad: ``` (k1 =+ v1) ((k2 =+ v2) f) ``` or ``` f |+ (k1,v1) |+ (k2,v2) ``` Recent p/printing hacking for a paper suggests that these...

mn200

As per the [GNU make specification](https://www.gnu.org/software/make/manual/html_node/Make-Control-Functions.html) if possible.

mn200

For backwards compatibility, there could be a theory-level command that turned this back off again, but I think monadsyntax should be available by default, perhaps binding to the `option` monad....

mn200