Изабель: Что, если для сеанса требуется более одного родительского сеанса? - PullRequest
Новая
       13

Изабель: Что, если для сеанса требуется более одного родительского сеанса?

0 голосов
/ 22 мая 2018

Я разработал набор теорий, в которых используются как Eisbach, так и библиотека HOL.Все отлично работает внутри Изабель / JEdit.Однако при попытке построить соответствующий сеанс с isabelle build Eisbach и библиотека HOL не найдены.Раньше, когда мне еще не была нужна библиотека HOL, я исправил это, указав HOL-Eisbach вместо HOL в качестве родительского сеанса в файле ROOT.В связи с необходимостью использования библиотеки HOL этот прием больше не работает, поскольку у вас не может быть более одного родительского сеанса.

Как можно создать сеанс, в котором одновременно используются Eisbach и библиотека HOL?

1 Ответ

0 голосов
/ 23 мая 2018

Вы можете указать дополнительные сеансы, от которых зависит ваш сеанс, в блоке sessions вашего файла ROOT, например (пример взят из AFP): 

session Zeta_Function (AFP) = Dirichlet_Series +
  options [timeout = 600]
  sessions
    Euler_MacLaurin
    Bernoulli
  theories [document = false]
    "Dirichlet_Series.Dirichlet_Series_Analysis"
  theories
    Zeta_Function
  document_files
    "root.tex"

Этот сеанс имеет Dirichlet_Series какродительский сеанс и дополнительно зависит от сеансов Euler_MacLaurin и Bernoulli.

Итак, как вы решаете, какие из ваших зависимостей должны быть родительским сеансом?Хорошо, имейте в виду, что для построения вашего сеанса родительский сеанс должен быть построен в первую очередь, но как только родительский сеанс станет доступным, вы можете просто использовать его без дополнительных затрат.Вот почему мы позволяем вещам зависеть от HOL по умолчанию: обычно он доступен предварительно.

Это также означает, что нет смысла выбирать сессию в качестве родителя, если вы используете тольконебольшая часть этого.Вот почему я не выбираю HOL-Library в качестве родительского сеанса.Обычно для этого требуется только одна или две теории, которые можно легко обработать в течение нескольких секунд, но если вы выберете ее в качестве родителя, пользователь должен построить все из HOL-Library, чтобыиспользуйте ваш сеанс.

Итак, я бы сказал, что вы должны выбрать родителя следующим образом:

  • Составьте список всех сеансов, от которых вы зависите и от которых вы используете значительныйколичество материала
  • Выберите самую большую сессию в этом списке в качестве родителя

Если родитель, с которым вы работаете, очень маленький (например, HOL-Eisbach), на самом деле вы этого не сделаетеполучить много от выбора его в качестве родителя.Вы можете сделать это, но вы также можете выбрать HOL.

...