#
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.
|