[ minor ] Bunch of minor updates and cleanups

.github/workflows/ci-deptycheck.yml

@@ -27,7 +27,6 @@ defaults:
     shell: bash
 
 env:
-  PACK_DIR: /root/.pack
   pack_dir_file: pack-dir.tar
 
 # TODO to reduce duplication, e.g. by using https://docs.github.com/en/actions/using-workflows/reusing-workflows
@@ -51,7 +50,7 @@ jobs:
       - run: ./.patch-chez-gc-handler idris2
 
       - name: Tar the `pack` dir
-        run: tar -cvf "${{ env.pack_dir_file }}" --exclude=".cache" "${{ env.PACK_DIR }}"
+        run: tar -cvf "${{ env.pack_dir_file }}" --exclude=".cache" "$PACK_DIR"
       - name: Save state of `pack`
         uses: actions/upload-artifact@v4
         with:
@@ -81,7 +80,7 @@ jobs:
       - run: pack install elab-util mtl-tuple-impls random-pure summary-stat
 
       - name: Tar the `pack` dir
-        run: tar -uvf "${{ env.pack_dir_file }}" --exclude=".cache" "${{ env.PACK_DIR }}"
+        run: tar -uvf "${{ env.pack_dir_file }}" --exclude=".cache" "$PACK_DIR"
       - name: Save built thirdparties
         uses: actions/upload-artifact@v4
         with:
@@ -112,7 +111,7 @@ jobs:
       - run: pack install deptycheck
 
       - name: Tar the `pack` dir
-        run: tar -uvf "${{ env.pack_dir_file }}" --exclude=".cache" "${{ env.PACK_DIR }}"
+        run: tar -uvf "${{ env.pack_dir_file }}" --exclude=".cache" "$PACK_DIR"
       - name: Tar built TTC files
         run: find "$(pwd)" -name '*.tt[cm]' | tar -uvf "${{ env.pack_dir_file }}" --files-from /dev/stdin
       - name: Save built DepTyCheck

.gitlab-ci.yml

@@ -1,7 +1,6 @@
 ---
 variables:
   GIT_SUBMODULE_STRATEGY: recursive
-  PACK_DIR: /root/.pack
 
 default:
   image: ghcr.io/stefan-hoeck/idris2-pack:latest

.pack-collection

@@ -1 +1 @@
-nightly-240128
+nightly-240207

.tbd.rst

@@ -1,14 +1,3 @@
-- Refactoring
-
-  - ``Test.Deptycheck.Gen.Auto`` -> ``Derivation.Deptycheck.Gen``
-
-- CI
-
-  - Сборка библиотеки deptycheck
-  - Сборка примера спецификации языка PIL
-  - Сборка положительных и несборка отрицательных примеров на языке PIL
-  - Генерация примеров на языке PIL при помощи библиотеки deptycheck
-
 - Отработка приёмов спецификации
 
   - Определённость значения переменной
@@ -21,24 +10,6 @@
 
     - Добавление свойства, что переменную можно использовать в выражении только когда она определена
 
-  - Конечность и dead-code
-
-    - Введение в описание statement'а понятия конечного statement'а,
-      то есть statement'а, после которого последовательная композиция будет dead-code
-
-    - Изменение правил композиции statement'ов с учётом нового параметра
-
-      - Последовательная композиция требует неконечный первым и её конечность совпадает с конечностью второго аргумента
-      - if-statement конечный только если обе ветки конечные
-      - while конечный, если его тело конечно
-      - и т.д.
-
-  - Return
-
-    - Введение понятия текущего возвращаемого типа
-    - Добавление нового типа statement'а -- return, -- который при этом является конечным statement'ом
-    - Добавление свойства, что тип выражения в return должен соответствовать типу текущего возвращаемого значения
-
   - Функция
 
     - Добавление спецификации на функцию определённой сигнатуры
@@ -58,12 +29,13 @@
     - Добавление типов statement'ов, соответствующим try-блокам и catch-блокам
     - Добавление свойства, что jump может осуществляться только в пределах try-блока и catch-блока
 
+  - Не нужно ли вместо statement'а последовательной композиции statement'ов иметь
+    отдельную сущность "последовательность statement'ов", то есть "линейный блок"?
+
 - Превращение рекурсивных ``Gen``'ов в Чёрч-кодированные, комбинирующиеся рекурсивными схемами.
   В частности, этим можно достигать хитрые комбинации, когда на определённой глубине корректных ``Gen``'ов используются специальные,
   генерирующие некорректные значения.
 
-- Автоматизация генерации ``Gen``'ов по спецификации структуры данных с зависимыми типами
-
 - Попытка разделения спецификации того, что есть в языке, от спецификации того, что нужно для пользовательских свойств.
 
   Например, в тип можно добавлять какое-нибудь пользовательское свойство, например, наличие конструкции ``if``
@@ -75,9 +47,3 @@
 - Параметром генератора может быть "тестовый набор, удовлетворяющий заданному критерию".
   Соответственно, по построению, генератор таких структур данных "тестовый набор" будет генерировать целиковые тестовые наборы,
   удовлетворяющие критерию.
-
-- Не нужно ли вместо statement'а последовательной композиции statement'ов иметь
-  отдельную сущность "последовательность statement'ов", то есть "линейный блок"?
-
-- Рассмотреть возможность ``Gen a`` быть лишь обёрткой над произвольным ``Monad m => Alternative m => m a``.
-  Соответственно, пляски с seed'ами и lazier list будут лишь частным случаем каких-то конкретных ``m``.

NOTICE

@@ -1,6 +1,6 @@
 DepTyCheck
-Copyright (c) 2020-2022 Denis Buzdalov
-Copyright (c) 2020-2022 Ivannikov Institute for System Programming
+Copyright (c) 2020-2024 Denis Buzdalov
+Copyright (c) 2020-2024 Ivannikov Institute for System Programming
                         of the Russian Academy of Sciences
 
 This Source Code Form is subject to the terms of the Mozilla Public