Разработка библиотеки Coq. (Добавить решение LoadPath недостаточно хорошо.) - PullRequest
Новая
       9

Разработка библиотеки Coq. (Добавить решение LoadPath недостаточно хорошо.)

0 голосов
/ 02 ноября 2018

Я добавляю некоторые теоремы в библиотеку https://github.com/coq-contribs/zfc

Но есть не очень хорошая вещь. Пока я разрабатываю код в CoqIDE, мне нужно добавить 

Add LoadPath "/home/user/0my/GITHUB/".

и переименовать все 

Require Import Axioms.

до 

Require Import ZFC.Axioms.

. Все файлы библиотеки находятся в 

/home/user/0my/GITHUB/ZFC

и имя последней папки имеет значение.

Но когда я хочу выполнить команду "make", мне нужно переименовать все обратно.

Файл «Make» содержит имена файлов и префикс. Удаление первой строки не решило проблему.

Я не думаю, что это лучшая практика разработки с CoqIDE, так что мне делать вместо этого?

Edited1:

У меня есть "run_coqide.sh", который состоит из 

#!/usr/bin/env bash
COQPATH=/home/user/0my/GITHUB/ 
/home/user/opam-coq.8.8.1/4.02.3/bin/coqide

«Из ZFC Require Import Sets.» Возникает ошибка «Не удается найти физический путь».

Edited2:

Я выяснил, что это рабочий скрипт: 

#!/usr/bin/env bash
export COQPATH=/home/user/0my/GITHUB/ 
/home/user/opam-coq.8.8.1/4.02.3/bin/coqide

Это обычный бег или взлом?

1 Ответ

0 голосов
/ 02 ноября 2018

Переименуйте Make в _CoqProject, это имя, в настоящее время распознаваемое CoqIDE, где оно будет искать конфигурацию проекта (в частности, параметр -R . ZFC, чтобы сделать файлы Coq в каталоге видимыми для CoqIDE). Также возможно изменить имя, которое ищет CoqIDE, на Make, но _CoqProject, похоже, действительно новый стандарт.

Обратите внимание, что опция -R . ZFC, позволяющая импортировать неквалифицированные библиотеки, соответствует команде Add Rec LoadPath "/.../ZFC" as ZFC.

Я бы также предложил на самом деле переключить всю кодовую базу на явную квалификацию ZFC.Axiom, которую вы выполняли локально вручную, что сделало ее менее подверженной ошибкам при работе с различными проектами одновременно. Я не уверен, почему было необходимо переименовать вещи для запуска make, я понимаю, что в этом не должно быть необходимости.

См. Также справочное руководство Coq, об утилите coq_makefile .

...