Collapse file tree

Files

 master

/

tools

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

Michael Norrish

Cope with Poly/ML that uses intinf as its int representation

Mar 9, 2021

5a979d2 · Mar 9, 2021

History

History

This branch is 2855 commits behind HOL-Theorem-Prover/HOL:master.

/

tools

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
Holmake		Holmake	Cope with Poly/ML that uses intinf as its int representation	Mar 9, 2021
cmp		cmp	Fix a number of Holmakefiles to use CLINE_OPTIONS	May 4, 2016
mllex		mllex	Extend unicode-grep to check for more style violations	Oct 22, 2018
mlyacc		mlyacc	Don't suggest we can compile with Moscow ML 2.01	Feb 28, 2019
mode-tests		mode-tests	emacs-mode: add an indentation bug to test-case file	Feb 25, 2021
quote-filter		quote-filter	Get Moscow ML quote filter to build given bb2fff9	Jan 20, 2020
sequences		sequences	Add examples/algorithms to build sequence	Feb 10, 2021
set_mtime		set_mtime	Give Holmakefiles access to a RELOCBUILD variable	Nov 28, 2017
trailing-wspace		trailing-wspace	Implement pure SML tool to detect and fix trailing whitespace	Aug 15, 2017
unicode-grep		unicode-grep	Allow Unicode lambda (λ, U+03BB) in src/	Aug 10, 2020
vim		vim	Update vim mode to cope with new SELECT_GOAL_LT syntax	Jan 5, 2021
win-binaries		win-binaries	Summary: tautLib upgraded to use HolSatLib engine.	Aug 8, 2007
yasnippets/sml-mode		yasnippets/sml-mode	Add some new snippets and make the emacs mode use company mode if pre…	Oct 13, 2017
.gitignore		.gitignore	Git-ignore a build file in tools	Jun 14, 2017
build-sequence		build-sequence	Get holyhammer to build with Moscow ML.	Aug 5, 2015
build.mlb		build.mlb	Refactor some .mlb files to get better sharing/modularity	Jun 14, 2017
build.sml		build.sml	Fix Moscow/ML build to cope with change in 0354d70	Jan 18, 2021
buildcline.sig		buildcline.sig	Improve build's behaviour when user's c/line options are bad	Oct 23, 2020
buildcline.sml		buildcline.sml	Improve build's behaviour when user's c/line options are bad	Oct 23, 2020
buildcline_dtype.sml		buildcline_dtype.sml	If build has no -j option, don't pass one to Holmake	Jan 17, 2021
buildhelp.txt		buildhelp.txt	Incorporate new c/line option-handling into build	Jan 29, 2017
buildutils.sig		buildutils.sig	Give build --dbg flag that gets passed on to Holmake	Sep 15, 2017
buildutils.sml		buildutils.sml	Holmake: can now (recursively) remove directories in EXTRA_CLEANS	Jan 21, 2021
check-intconfig.sml		check-intconfig.sml	Adaptations in preparation for the release of Poly/ML 5.6.	Jan 6, 2016
configure-mosml.sml		configure-mosml.sml	Don't suggest we can compile with Moscow ML 2.01	Feb 28, 2019
configure.sml		configure.sml	Change version numbers for Kananaskis-14	Jan 6, 2021
documentation-directories		documentation-directories	Moved documentation from src/*/help/entries directories to help/Docfi…	Aug 6, 2010
end-init-boss.sml		end-init-boss.sml	Move DefnBase to src/coretypes, make progress with one_line_ify	Jan 10, 2020
end-init.sml		end-init.sml	This file turns the printing of declarations back on in MoscowML. This	Oct 27, 1999
hol-input.el		hol-input.el	emacs-mode: put ⦇ and ⦈ under hol-input's \( and \) maps	Mar 19, 2020
hol-mode.sml		hol-mode.sml	hol-mode: add hol-print-info	Apr 24, 2017
hol-mode.src		hol-mode.src	Enable builtin emacs tech for displaying tooltips in minibuffer	Mar 4, 2021
hol-unicode.el		hol-unicode.el	Avoid combining star for RTC operator; use Slavonic Asterisk instead	Sep 2, 2020
holscript-mode.el		holscript-mode.el	emacs-mode: fix indentation bug identified in c3e0ecb	Feb 28, 2021
holwrap.py		holwrap.py	Holwrap (HOL-Theorem-Prover#758)	Dec 18, 2019
make_iss.sml		make_iss.sml	Tweak generation of Inno Setup file for building Windows installer	Nov 11, 2014
makefile.muddy.src		makefile.muddy.src	Removed extra occurrence of CFLAGS so that MuDDy Makefile is generate…	Jul 14, 2007
mlton-build.sml		mlton-build.sml	MLton implementation of build	Jun 14, 2017
smart-configure.sml		smart-configure.sml	Ensure HOL4 works with fixed-width integers under Poly/ML.	Feb 15, 2016
unquote-init.sml		unquote-init.sml	Make pretty-printer use Unicode delimiters by default	May 23, 2017
win-config.sml		win-config.sml	Make win-config's handling of sigobj/SRCFILES idempotent.	Oct 10, 2012
View all files