History log of /seL4-l4v-10.1.1/HOL4/tools/Holmake/tests/gh604/base/base1Script.sml
Revision Date Author Comments
# 54867513 15-Oct-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Add files demonstrating problem with interactive use of INCLUDES

This is github issue #604.

Problem is that Holmake will correctly build finalTheory, but an
interactive hol session will fail to load base2Theory because the
session's loadPath only points to mid. The session would also fail to
load base1Theory, but can get at it successfully via midTheory.

A workaround is to augment the Holmakefile's INCLUDES line. The proper
fix is to have interactive sessions set up INCLUDES info (augmenting
loadPath) in the same way that Holmake does.

Not yet a test as I haven't a fix to hand, and haven't got the
scripting set up to test the interactive behaviour either.