Есть ли примеры источников Изабель для научных работ c?

Question

Я завершил лучшую часть основной разработки в Isabelle и задаюсь вопросом, как лучше go написать соответствующую академическую c работу.

Из источников Изабель я могу составить несколько своеобразный c взгляд на такую ​​бумагу. Однако стандартное отображение теорем, лемм и определений почти наверняка оттолкнет рецензентов.

Теории LaTeX-сахара помогают, но, по-видимому, только если я вручную переформулирую всю теорию, используя анти-цитаты.

Есть ли примеры разработок Изабель, лежащих в основе публикаций, на которые я могу вдохновиться, как лучше всего действовать здесь?

Answer 1

Я делал это в прошлом (для моей магистерской диссертации), есть только один случай, когда вы должны это сделать: документация Изабель и документация разработок Изабель (например, AFP).

Есть люди, которые это делают (Макариус Венцель, например, https://sketis.net/2019/11), аналогично «Конкретной семантике». Однако это не лучшее решение.

Причины, по которым этого не следует делать:

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

2. Если вы не набираете макросы LaTeX напрямую, вы гораздо более ограничены в своих возможностях (с точки зрения LaTeX). И если вы вводите латексные макросы напрямую, вы больше не можете создавать вывод HMTL. Таким образом, выгода Изабель ограничена.

3. Многие конференции хотят видеть исходники LaTeX, но они не запускают Изабель, поэтому вам все равно придется сгенерировать LaTeX (и даже, возможно, сделать некоторые эффекты постпродакшена, потому что Изабель не может делать некоторые вещи).

4. Вы редко хотите использовать точную теорему Изабель (LaTeXsugar может помочь, но это не идеально) .

5. Что, если вы напишете статью сейчас и обнаружите опечатку, которую хотите исправить через 5 лет? Через 5 лет латекс будет работать. Isabelle2020, вероятно, нет.

6. Все ли ваши соавторы используют Isabelle на всех своих компьютерах, в том числе на вашем ноутбуке, если вы в отпуске и вам нужно что-то сделать? *

7. И вы будете часто драться с Изабель, например:

   text "\ begin {counterexample}"

   lemma True by auto

   text " \ end {counterexample} "

   не работает, потому что текст - это отдельная среда, поэтому вам нужны эффекты постпроизводства.

В основном, используйте механизм фрагментов для извлеките LaTeX из теорий, а затем используйте свой любимый редактор LaTeX.