Как пропустить (проблемные) сеансы Isabelle в AFP?

#isabelle

Вопрос:

Я пытался использовать AFP (22.02.2021) с Isabelle 2021, но jEdit / Isabelle PIDE не загружался после добавления каталога AFP в корневой файл пользователя. Показано ниже и, похоже, касается конкретного пакета:

Мне действительно не нужна рассматриваемая запись (или я не знаю, что она делает). Мой вопрос:

Есть ли способ использовать подмножество AFP и исключить проблемные записи на скриншоте?

— Обновить —

Как указано в комментариях, AFP, похоже, отстает на пару дней. Использование afp-02-24-2021 , первоначальная ошибка исчезла. Однако при выборе сеанса Jordan-Normal-Form из jEdit появляется новая ошибка о JNF-AFP-Lib сбое сборки, как показано ниже:

Вопрос остается. AFP, похоже, представляет собой большую коллекцию, и может быть несколько источников ошибок.

В случае таких ошибок есть ли способ выбрать подмножество AFP для использования или отладки?

Если нет, есть ли систематический способ проверить, какие afp создают или не создают?

1. Используете ли вы дистрибутив AFP-2021?

2. @larsrh, да, я загрузил afp-current одновременно с загрузкой Isabelle 2021.

3. AFP отстает на несколько дней, попробуйте загрузить сегодняшний пакет. Возможно, вы все еще поймали AFP на 2020 год.

4. Да, приведенное выше сообщение об ошибке определенно все еще AFP-2020. Как сказал Ларс, AFP всегда выпускается через несколько дней после выхода Isabelle, а AFP-2021 только что вышел, поэтому, если вы повторно загрузите его, он должен работать.

Ответ №1:

Оригинальный вопрос

Проблема заключалась в том, что вы (по незнанию) использовали выпуск AFP, который не соответствовал выпуску Isabelle. Чтобы избежать этой проблемы в будущем, я рекомендую использовать репозиторий Mercurial напрямую:

https://foss.heptapod.net/isa-afp/afp-2021

Репозиторий Mercurial для новой версии Isabelle создается на этапе RC, поэтому вы всегда можете быть уверены, что у вас есть соответствующие версии.

В случае этих несоответствий обычно невозможно выбрать подмножество AFP, которое «работает», потому что в период с 2020 по 2021 год управление сеансами значительно изменилось.

Обновить

Проблема, с которой вы сталкиваетесь здесь, заключается в том, что вы выбрали большой сеанс в качестве предварительного условия, и сборка с конфигурацией по умолчанию занимает слишком много времени.

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

 isabelle build -bv -d <path to afp>/thys -o timeout_scale=3 Jordan_Normal_Form

Увеличьте коэффициент, если он сохраняет время ожидания.

Общее замечание

Вы спрашиваете: «В случае таких ошибок, есть ли способ выбрать подмножество AFP для использования или отладки?». Ответ на этот вопрос зависит от типа ошибки. В настоящее время ваш пост содержит две совершенно разные проблемы, поэтому, к сожалению, дать общий ответ невозможно.