Минимальный WYSIWYG-процессор для проверки в стиле Fitch с бэкэндом LaTeX

Question

Я не уверен, подходит ли это лучше для TeX.SE или Stackoverflow, но, учитывая, что он в основном ориентирован на TeX, я решил, что коллективный разум TeX здесь подойдет лучше всего.

Мне бы хотелось иметь графический процессор документов для написания логических доказательств в стиле Fitch, подобных тем, которые создаются с помощьюПакет LPLFitch. Я бы хотел, чтобы он был полностью WYSIWYG (что видишь, то и получаешь), не требуя от пользователя прямого взаимодействия с кодом TeX, но используя LaTeX в бэкэнде. Кроме того, я бы хотел, чтобы он был полностью автономным, не требуя установки LaTeX на компьютере пользователя. Он бы использовался для помощи студентам, не имеющим опыта работы с TeX, в создании таких доказательств.

У меня вопрос, какие существуют ресурсы с открытым исходным кодом? Единственное, с чем я знаком, этоЛиКс, но это нацелено на полномасштабную реализацию LaTeX, в отличие от минимального процессора, который я имею в виду и который будет использовать лишь очень небольшое количество пакетов и минимальный набор полной мощности LaTeX.

Цель:

1. Процессор документов, работающий по принципу WYSIWYG.
2. Будет иметь несколько кнопок для вставки необходимых символов и будет немедленно отображать эти символы (либо вставляя их как символы Unicode, либо выполняя быструю компиляцию).
3. Не требует знания LaTeX на стороне пользователя и не требует полной установки LaTeX на компьютерах пользователей.
4. Создаст доказательства естественного вычета в стиле Fitch, подобные тем, что есть в пакете LPLFitch.

Вопросы:

1. Какие существующие ресурсы с открытым исходным кодом я мог бы использовать для своей работы?
2. Какой совет вы бы дали для реализации чего-то подобного с нуля (например, использовать LuaTeX или какую-то более программную разновидность TeX)?
3. Это вообще хорошая идея, или я просто позволяю своему знакомству с LaTeX не замечать лучших решений?

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

Answer 1

Два веб-сервиса делают что-то примерно похожее на то, что задается в вопросе. В обоих случаях сервис поддерживает какой-то экспорт TeX; однако ни один из них не использует пакет, lplfitchуказанный в исходном вопросе.

• FitchJS(смотрите такжеживая версия) экспортируется в формат с использованием fitch.styпакета Йохана Клювера. (Копия доступна наLogicMattersа также в репозитории Git для fitchjsпроекта.)
• Proofmoodвыходы в их собственныхпользовательский формат; но не ясно, является ли их код открытым. (Разработка корейской версии также, по-видимому, ведется более активно по сравнению с английской версией.)

Вполне возможно создать форк FitchJSи заставить его использовать lplfitch: код для обработки генерации LaTeX находится в двух файлах:

1. В parsing.jsнем есть часть, в которой символы Unicode преобразуются в их эквиваленты LaTeX и обратно. lplfitchДля связок используются разные микрокоманды; эту часть должно быть легко исправить.

2. Немного сложнее процедура экспорта в userio.js; синтаксис для fitchпакета существенно отличается от синтаксиса для добавления строки проверки в lplfitchпакет и потребует немного больше времени для переписывания.

   (Похоже, что доказательство хранится во внутреннем стеке (если мой беглый взгляд верен), в таком случае, возможно, лучше сбросить существующую процедуру экспорта и написать что-то новое, основанное на преобразовании доказательств сначала в строки, а затем на преобразовании отдельных строк (включая правильное количество вертикальных черт) в одну строку на выходе, полностью игнорируя логическую структуру. Это полная противоположность тому, что lplfitchтребуется.)