search

Twigonometry / IsabelleDSL

IsabelleDSL (iDSL) is a framework for generating Domain-Specific Languages from specifications written in Isabelle
0 stars 0 forks source link

Fix imports of theories outside current directory #24

Open Twigonometry opened 2 years ago

Twigonometry commented 2 years ago

Isabelle behaves strangely when specifying imports outside of the current directory:

session Stack = "HOL-Library" +
  theories
    Stack
    "/tmp/StringUtils"
  export_files (in ".") "*:**.hs"

Gives error Cannot load theory file "/home/mac/Documents/Diss/IsabelleDSL/Theories/Stack/StringUtils.thy", which seemingly ignores the specification of /tmp. The same happens with trying to access "/home/mac/Documents/Diss/IsabelleDSL/Resources/StringUtils" (the path to the permanent version of StringUtils.thy on my system).

Twigonometry commented 2 years ago

Not crucial to fix this, as the theory builds when all theories are copied across to /tmp. However, it is frustrating when trying to manually test the theory files, as StringUtils.thy must be copied to the working directory