Может ли Изабель импортировать файлы в каталог, где в имени есть пробел?

Question

Я использую Google Drive для хранения теорий, но хочу использовать разные каталоги для разных тем. Но import "/ Users / dstr / Google Drive / Isabelle / Galois / PreGalois" не работает, поэтому я установил переменную среды $ ISABELLEWORK и обнаружил import "$ ISABELLEWORK / Galois / PreGalois" не работает, так как переменная окружения не распознается Изабель.

У меня два вопроса: один, возможно ли импортировать теории из каталогов с пробелами "Google Drive"? Второе, можно ли заставить Изабель распознавать новые переменные среды? большое спасибо

Answer 1

Вы не можете импортировать теорию с пробелом в пути ..., если она не определена в переменной.

Отредактируйте файл ~ / .isabelle / Isabelle2019 / etc / settings (замените 2019 на версию Isabelle, которую вы используется, вам, возможно, придется создать файл) и добавить строку

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

Перезапустите Изабель, и импорт "$ ISABELLEWORK / Galois / PreGalois" будет работать.