Coq: проблема с требованием экспорта - PullRequest
Новая
       63

Coq: проблема с требованием экспорта

2 голосов
/ 25 сентября 2019

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

> From LF Require Export Basics.

Что бы я ни пытался, я всегда получаю следующий ответ:

"Не могу найтифизический путь, связанный с суффиксом соответствия логического пути <> и префиксом LF. "

Я скомпилировал Basics.v из coqIde, и файл Basics.vo создан правильно.Я также скомпилировал его из командной строки coqc, как и предполагалось, где-то находится мой файл _CoqProject, в той же папке, что и Basics.v, и заявляет: -Q . LF для параметра _CoqProject установлено значение «добавлено в аргументы».

когда я загружаю Basics.v, я вижу в нижней части CoqIde «Параметры чтения из ..._ CoqProject», я помещаю папку lf в папку, которая находится в LoadPath coq.

Что еще можно проверить?

Моя система - Windows 10. Я запускаю CoqIde 8.9.1

Спасибо!

1 Ответ

1 голос
/ 26 сентября 2019

Я обычно работаю на машине с Linux, но здесь что-то, что я делал с помощью виртуальной машины.

  1. Я скачал установщик Windows из https://github.com/coq/coq/releases/tag/V8.9.1
  2. Я загрузил lf.файл tgz из https://softwarefoundations.cis.upenn.edu/lf-current/index.html
  3. Я запустил установщик Windows для Coq.Он поместил систему coq в C: \ coq
  4. Я использовал cygwin инструменты, чтобы развернуть файл lf.tgz, чтобы у меня был каталог C:\Users\user\foundations\lf, содержащий Basics.v, _CoqProject и т. Д.

Затем я использовал команду поиска, чтобы найти coqide в качестве установленного приложения.Затем я выполнил следующие действия:

  1. start coqide
  2. , откройте файл Basics.v
  3. , используйте опцию Compile-> Compile buffer

Затем я мог заметить, что каталог C:\Users\user\foundations\lf содержит файл с именем Basics.vo

Затем я открыл новый буфер и написал From LF Require Export Basics. и не попытался выполнить эту строку Я сохранил этот буфер в файле в каталоге C:\Users\user\foundations\lf.Давайте предположим, что этот файл называется toto.v Я закрыл буфер toto.v. Я заново открыл toto.v, используя опцию File-> Open Я выполнил содержимое файла.

Этот процесс является результатом проб и ошибок.Что я знаю, так это то, что Require Export ... работает, только если на вашем диске есть ...vo файлы, но coqide нужно знать, где искать эти файлы.Для этого он поддерживает «путь загрузки».При открытии файла из данного каталога coqide просматривает этот каталог (и его предков), чтобы найти файл _CoqProject, и последний может содержать директивы для изменения пути загрузки.Здесь дело обстоит так: «-Q. LF» указывает, что все .vo файлы в текущем каталоге должны быть рассмотрены, и что их символическое имя должно начинаться с префикса «LF».

Проблема в том, что когдавы начинаете с пустого буфера, никакой файл _CoqProject не читается и не находит, где искать ваши данные.Вот почему я сделал шаги 5-6-7: при чтении файла toto.v я спровоцировал чтение файла _CoqProject.

Урок на вынос: убедитесь, что файл Basics.vo существует,и затем убедитесь, что буфер, над которым вы работаете, был получен с помощью операции чтения из того же каталога.При необходимости сохраните, закройте и снова откройте, чтобы убедиться в этом.

...