Can't `open compilerTheory` in HOL

[hjorthjort]

After downloading a fresh copy of CakeML (as well as PolyML and HOL) and running Holmake in the compiler directory, I can't source compilerTheory or lexer_funTheory.

Here is what happens.

root@21574aeebe3f:~/cakeml/compiler# hol

---------------------------------------------------------------------
       HOL-4 [Kananaskis 11 (stdknl, built Wed Mar 22 08:59:47 2017)]

       For introductory HOL help, type: help "hol";
       To exit type <Control>-D
---------------------------------------------------------------------
[extending loadPath with Holmakefile INCLUDES variable]
[In non-standard heap: /root/cakeml/compiler/heap]
> open compilerTheory;
poly: : error: Structure (compilerTheory) has not been declared
Found near open compilerTheory
Static Errors
> open lexer_funTheory;
poly: : error: Structure (lexer_funTheory) has not been declared
Found near open lexer_funTheory
Static Errors
> 

I have tried this on a fresh machine as well, by creating a docker image. Here is the Dockerfile, which should be failry intelligible even if you don't have experience with Docker. It does the following:

• From a fresh ubuntu machine ...
• I RUN a few select commands to set up CakeML ...
• And then log onto the machinge, go to the compiler directory, and run hol as above.

FROM ubuntu:latest

# Get dependencies
RUN apt-get -y update
RUN apt-get install -y git gcc g++ make vim

# Install CakeML and all dependencies
RUN cd ~
RUN git clone https://github.com/CakeML/cakeml.git
RUN cd cakeml && ./build-instructions.sh

# Make project
ENV PATH /root/HOL/bin:/root/poly:$PATH
RUN cd ~/cakeml/compiler/backend && Holmake --fast
RUN cd ~/cakeml/compiler/ && Holmake --fast

CMD cd ~/cakeml/compiler && echo "echo open compilerTheory | hol" ; echo "echo open backendTheory | hol"

Known working and non-working theories:

Non-working:

• compilerTheory
• lexer_funTheory

  Working

• astTheory
• preamble
• backendTheory
• modLangTheory

Note that I am using the fast build of Holmake. I am trying this again right now, once again from a fresh copy, where I will use Holmake without the --fast flag.

This problem appeared locally in my development environment yesterday, March 21.

[xrchz]

Can you try load "compilerTheory"; first?

[hjorthjort]

That worked, for both compilerTheory and lexer_funTheory

[xrchz]

By the way, the editor support in vim and emacs can help do these loads automatically. I guess this issue is closed now, reopen if not.

[hjorthjort]

Originally I encountered this problem when trying to source lexer_funTheory from the vim plugin.

I'd say it's closed. Big thanks!

[xrchz]

You might need to use the hl or hL commands in the vim plugin (as mentioned in its README) to get it to call load.