Описание тега coqide

Вопросы с тегом
Графический интерфейс (IDE) для Coq. Он написан на OCaml.
1 ответ

Конфигурация CoqIDE в Linux

У меня свежая установка Coq 8.6 в Ubuntu 17.04. Когда я пытаюсь скомпилировать свой проект, используя make, он работает нормально, пока не получит первое сообщение об ошибке. Затем я пытаюсь использовать CoqIDE, чтобы найти и исправить ошибку, но я …
11 май '17 в 19:04
2 ответа

Как установить Coq

Я устанавливал Coq, используя ссылки для скачивания с https://coq.inria.fr/ для Windows и Mac. Тем не менее, когда я пытаюсь coqc или же coqtop в терминале или командной строке я получаю сообщения об ошибках, в которых говорится, что команда не найд…
25 янв '17 в 16:37
1 ответ

Learning coq, не уверен, что означает ошибка NNPP

Так что я только начал изучать coq (и это пока слишком далеко), и я пытаюсь сделать базовое доказательство, и я довольно потерян, нашел некоторую помощь до сих пор, но я думаю, что я должен делать coq выдает ошибку. Итак, в моей части редактора у ме…
27 фев '19 в 02:40
0 ответов

CoqIDE Make на Windows

У меня есть GnuWin32 Make и GnuWin32 Coreutils, установленные и установленные на моем компьютере. PATH, Это работает: coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq Frap.vo Но если я открою Frap.v в CoqIDE и выполните Compile> Make…
11 ноя '17 в 21:08
2 ответа

Coq makefile "Top". Префикс

Я использую автоматический генератор make-файлов Coq 8.5. Этот makefile ставит перед всеми модулями префикс "Top"., Теперь предположим, что вы запускаете много файлов по make, а затем хотите изменить / отладить некоторый файл в IDE. Тогда раздражает…
31 мар '17 в 10:46
1 ответ

CoqIDE ошибка с экспортом модулей в той же библиотеке

Я использую CoqIDE, чтобы прочитать серию учебников "Основы программного обеспечения", в настоящее время читаю том "Логические основы". Я только начал главу 2 (Индукция), но когда я пытаюсь запустить линию From LF Require Import Basics. Я получаю со…
17 дек '18 в 20:46
1 ответ

Установка CoqIDE - Ошибка обновления jhbuild

У меня уже установлен Coq, сейчас я пытаюсь установить CoqIDE на Mac. Я следую за Coq вики. Сборка не удалась на втором этапе. Когда я бегу sh gtk-osx-build-setup.sh Это ошибка, которую я получаю: Checking out jhbuild (<!DOCTYPE HTML PUBLIC "-//I…
30 май '18 в 16:38
0 ответов

CoqIde: показать, что делает простая тактика

Используя CoqIde, есть ли способ просмотреть шаги simpl взят? Я нахожу, что не понимаю, как он достиг своего результата довольно часто. Пример: rev (rev (n :: l')) = n :: l' -- apply simpl. rev (rev l' ++ [n]) = n :: l'
12 янв '19 в 10:11
1 ответ

Ссылка "X" не найдена в текущей среде

Я использую CoqIDE для выполнения упражнений в книге "Основы программного обеспечения" о Coq. Я могу успешно скомпилировать Basics.v, в результате чего в моем каталоге появятся Basics.vo и Basics.glob. Когда я пытаюсь запустить Induction.v, это рабо…
19 окт '16 в 10:55
0 ответов

Coq: нотация не напечатана

Я определил индуктивный тип, минимальный пример ниже. Я хотел бы использовать обозначения, такие как ~ или =. Синтаксис распознается, но не печатается в целях верхней правой панели. Пример: Inductive num : Set := | O : num | S : num -> num. Theor…
19 дек '18 в 10:00
0 ответов

Basics.vo содержит основы библиотеки, а не библиотеку Metalib.Basics

Я получаю ошибку "Basics.vo содержит основы библиотеки, а не библиотеку Metalib.Basics" в CoqIDE 4.5. Я следую Основам программного обеспечения и импортирую Основы как "Требуются Основы экспорта". Также я скомпилировал основы, используя тот же CoqID…
13 фев '19 в 07:48
1 ответ

Как разделить код Coq для подачи Coq ideslave (протокол XML)?

Я думал, что вызов "Добавить" Coq ideslave (также известный как протокол Coq XML) занимает один кусок кода за раз, разделенный по периодам (.). Я все еще верю, что это правда в большинстве случаев. Например, Inductive or (A B:Prop) : Prop := | or_in…
19 дек '17 в 04:34
1 ответ

Как получить оригинальную привязку клавиш для Coq?

Я изменил привязку клавиш в соответствии с: https://github.com/coq/coq/wiki/Configuration-of-CoqIDE но теперь я не могу вернуть их в нормальное состояние. Как мне их в состояние по умолчанию? Обратите внимание, что Coq уже изменил файл, и я не могу …
05 ноя '18 в 04:59
2 ответа

Плагин Vim не распознает существующую поддержку Perl

Я использовал плагин CoqIDE для Vim на компьютерах с Linux для редактирования файлов Coq. Сейчас я пытаюсь установить его на Windows 8. Но когда я пытаюсь найти плагин, я получаю Your vim doesn't support Perl. Install it before using CoqIDE mode. чт…
20 июл '14 в 16:42
0 ответов

Указание пути coqtop для плагина CoqIDE Vim в Windows 8.1

Я пытаюсь заставить плагин CoqIDE Vim работать на Windows 8.1. Когда я получаю плагин от Vim, я получаю следующее сообщение об ошибке: coqtop.opt: command not found. Поэтому я посмотрел документацию по плагину и нашел часть, которая кажется подходящ…
23 июл '14 в 13:55
1 ответ

Извлечение Coq: отказано в разрешении

Когда я выполняю следующие команды в CoqIDE: Extraction Language Haskell. Extraction "Code.hs" my_function. Я получаю следующую ошибку: System error: "Code.hs: Permission denied" Если я попробую вместо этого: Extraction Language Haskell. Extraction …
18 дек '15 в 05:54
1 ответ

Как настроить цвета для Command и Tactic в ProofGeneral при использовании Coq в Emacs?

Я хочу раскрасить какую-то конкретную команду и тактику в другой цвет, например, я хочу, чтобы команды "Печать" и "Найти" были серыми, а "индукция" - каким-то особым цветом, отличным от других тактик. Возможно ли это в ProofGeneral? Если это не наст…
09 окт '18 в 03:08
1 ответ

Задать печать юниверсов не имеет никакого эффекта

Я следую за главой "Юниверсы" в cpdt ( http://adam.chlipala.net/cpdt/html/Universes.html), в которой Set Printing Universes. чтобы увидеть дополнительные комментарии по типам. Тем не менее, я использую CoqIde 8.6, и это не имеет никакого эффекта. Сл…
03 фев '18 в 23:50
2 ответа

Coqide 8.5: нет подсветки синтаксиса в Linux

Я установил Coqide 8,5 Вт / nix, К сожалению, текст blakc во всех панелях; нет никакой подсветки синтаксиса (в противном случае 8.5 кажется большим улучшением по сравнению с 8.4, который я также установил). Я также получаю следующее: (coqide:17272):…
18 июн '16 в 21:33
2 ответа

Агда-подобное программирование в Coq/Proof General?

В отличие от Agda, Coq стремится отделить доказательства от функций. Тактика, которую дает Coq, отлично подходит для написания доказательств, но мне интересно, есть ли способ воспроизвести некоторые функциональные возможности режима Agda. В частност…
24 янв '17 в 19:55