import - Isabelle 可以在名称中有空格的目录中导入文件吗？

Question

我正在使用“Google Drive”来存储理论但想为不同的主题使用不同的目录。但是 导入“/Users/dstr/Google Drive/Isabelle/Galois/PreGalois” 无法正常工作，所以我设置了一个环境变量 $ISABELLEWORK 并发现 导入“$ISABELLEWORK/Galois/PreGalois” 不起作用，因为无法识别环境变量通过伊莎贝尔。

我有两个问题：一，是否可以从带有空格“Google Drive”的目录中导入理论？二、我能让Isabelle识别新的环境变量吗？非常感谢

标签： importisabelle

Answer 1

您不能导入路径中带有空格的理论……除非它在变量中定义。

编辑文件 ~/.isabelle/Isabelle2019/etc/settings （将 2019 替换为您正在使用的 Isabelle 版本，您可能需要创建文件）并添加该行

ISABELLEWORK="/Users/dstr/Google Drive/Isabelle/"

重新启动 Isabelle 并导入 "$ISABELLEWORK/Galois/PreGalois" 将起作用。