flang 0.7.28 — Примеры в законах проверяются, ошибки в категориях находятся при компиляции

Примеры в законах проверяются, ошибки в категориях находятся при компиляции

Что появилось

• flang test и flang check прогоняют примеры внутри блока закон. Раньше такие примеры не запускались вовсе, и неверное ожидание в них проходило молча. Теперь пример с неверным ожиданием даёт код 1, а сообщение называет закон, пример, ожидаемое и полученное значение: ожидалось {"номер":777}, получено {"номер":500}.
• check проверяет, как собрана категория. Стрелка, которой нет среди объявленных, стрелка, названная дважды, композиция через стрелку не из этой категории, концы стрелок, которые не сходятся, — всё это теперь ошибка с кодом 1 и номером строки. Например: FLANG_CATEGORY_UNKNOWN_ARROW в файле warehouse.flang, строка 9, столбец 1: категория «Склад»: стрелки «потерять» не объявлено.
• check --proof объясняет, почему не доказал равенство из длинной цепочки вызовов. Подстановка доказанных свойств функций делает не больше 64 шагов. Если их не хватило, утверждение остаётся недоказанным, и ответ говорит прямо: переписка доказанными равенствами исчерпала «Предел переписки» — 64 шага. Раньше было только «объявлено, не доказано» без причины.
• Обе проверяющие программы (на C и на Lean 4) перепроверяют утверждения с квантором внутри и притом и если. Такие утверждения ядро доказывало и раньше, теперь их доказательство перепроверяется независимо.

Что изменилось

• Файл с категориями, где все законы проверены, проходит check с кодом 0. Раньше любой такой файл получал код 2 с припиской, что устройство категорий не проверяется. Из 25 примеров в flang/ct с кодом 0 теперь проходят 16, было 7. Остальные 9 получают код 2 и называют закон, который не удалось проверить.
• check --proof по стандартной библиотеке стал немного быстрее. Ядро берёт доказанные свойства только у тех функций, которые встречаются в доказываемом утверждении. На 55 файлах flang/stdlib суммарное время 5773 с у 0.7.27 и 5518 с теперь, то есть на 4 % меньше; результаты проверки те же.

Что сломалось

• Неверный пример в блоке закон теперь роняет test и check с кодом 1. Исправьте ожидаемое значение в примере или саму функцию: сообщение называет оба значения.
• Ошибка в устройстве категории — теперь код 1 у check, а не 2. Объявите недостающую стрелку через морфизм или уберите её из блока категория; повторную строку удалите.

Описание языка

Разделы DESCRIPTION.md с v0.7.27 не менялись.

---

Examples inside laws run, mistakes in categories are caught at compile time

What appeared

• flang test and flang check run the examples inside a закон (law) block. These examples never ran before, so a wrong expectation passed silently. Now a wrong expectation is exit code 1, and the message names the law, the example, the expected and the actual value: ожидалось {"номер":777}, получено {"номер":500}.
• check verifies how a category is put together. An arrow that was never declared, an arrow listed twice, a composition through an arrow outside the category, arrow ends that do not meet are now errors with exit code 1 and a line number. For example: FLANG_CATEGORY_UNKNOWN_ARROW в файле warehouse.flang, строка 9, столбец 1: категория «Склад»: стрелки «потерять» не объявлено.
• check --proof says why an equality over a long chain of calls was not proved. Substituting proved properties of functions takes at most 64 steps. When that is not enough, the statement stays unproved and the answer says so: переписка доказанными равенствами исчерпала «Предел переписки» — 64 шага (rewriting ran out of its 64-step limit). Before, you only got "declared, not proved" with no reason.
• Both proof checkers (in C and in Lean 4) re-check statements with a quantifier inside и притом (and) and если (if). The kernel proved such statements before; now their proofs are re-checked independently.

What changed

• A file with categories whose laws were all checked passes check with exit code 0. Before, every such file got code 2 with a note that category structure is not checked. Of the 25 examples in flang/ct, 16 now pass with code 0, up from 7. The other 9 get code 2 and name the law that could not be checked.
• check --proof over the standard library is a little faster. The kernel takes proved properties only from the functions that appear in the statement being proved. Over the 55 files of flang/stdlib the total time is 5773 s on 0.7.27 and 5518 s now, 4 % less, with the same results.

What broke

• A wrong example in a закон block now fails test and check with exit code 1. Fix the expected value in the example or the function itself; the message names both values.
• A mistake in how a category is built is now exit code 1 from check, not 2. Declare the missing arrow with морфизм or drop it from the категория block; delete a repeated line.

---

Страница выпусков: по-русски · in English.

Архив flang-0.7.28-c.tar.gz — исходники C99 и Makefile: make && sudo make install, Node не нужен. Или brew install digitable-lol/tap/flang.