Запуск приложения Hello World в Agda emacs

Я установил компилятор Agda, бинарные файлы можно найти здесь: http://ocvs.cfv.jp/Agda/how-to-install-windows.html.

... и я пытаюсь заставить его скомпилировать простое приложение hello world (я нашел в Интернете код Agda 'Hello World')

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

open import System.IO using ( _>>_ ; putStr ; commit )

module System.IO.Examples.HelloWorld where

main = putStr "Hello, World\n" >> commit

Я ищу пошаговые инструкции по запуску простой программы Hello World

Компилятор Agda Emacs

Рабочий пример с другим компилятором также будет приемлемым ответом

Спасибо!


emacs agda
person Adjam    schedule 18.06.2018    source источник
comment
Вы читали документы?   -  person user2407038    schedule 20.06.2018
comment
У меня есть сейчас, но мне нужно базовое пошаговое руководство   -  person Adjam    schedule 21.06.2018
comment
Пожалуйста, отредактируйте свой вопрос, включив сообщение об ошибке в виде текста, чтобы мы могли скопировать / вставить его и чтобы Google мог его найти. .   -  person tripleee    schedule 21.06.2018
comment
Также покажите, что именно вы сделали, чтобы появилось это сообщение об ошибке. Вы набирали такую ​​команду, как M-x compile, или использовали какую-то последовательность нажатия клавиш, например C-c C-c?   -  person tripleee    schedule 21.06.2018

Ответы (3)


arrow_upward
0
arrow_downward

Похоже, вы пытались использовать что-то вроде общих M-x compile, а не каких-либо конкретных функций Agda.

Индикатор режима Agda:run в строке режима Emacs предполагает, что у вас есть запущенный процесс Agda в другом буфере, но вы не смотрите на него. В режиме Agda, вероятно, есть что-то вроде agda-eval-buffer, которое должно передавать текущую программу этому процессу и отображать результаты в нижней половине панели. (Попробуйте вручную переключиться на буфер с именем типа *inferior-agda*, если вы каким-то образом не можете добраться до этого буфера другими способами.)

На сайте, на который вы ссылаетесь, указано, что это Agda 1, и вам, вероятно, действительно стоит поискать Agda 2 на другом сайте.

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

Сообщение об ошибке указывает на то, что вам необходимо установить make.

Я предполагаю, что после того, как вы исправите эту, могут быть дополнительные недостающие зависимости. В идеале документация должна четко указывать, что именно вам нужно установить.

make - это просто оболочка для запуска любых бакланов, находящихся в локальном Makefile. Если такого файла нет, вы, вероятно, захотите изменить команду компиляции на что-то другое. (Обычно Emacs запрашивает команду для запуска, но предоставляет вероятное значение по умолчанию.)

person tripleee    schedule 21.06.2018

arrow_upward
0
arrow_downward

Учитывая, что я работаю в Linux и не являюсь экспертом по agda, это решение может не того стоить. Но все же я попробую.

Когда я установил agda и agda-stdlib в свою систему, он предоставил мне файл с именем agda2.el в /usr/share/agda/emacs-mode. При этом в моем ~/.emacs.d/init.el файле было только что:

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

Поскольку у вас уже есть настройка режима agada в Emacs, вышеуказанное не будет полезно, если ваша версия режима agda не устарела.

Мы можем скомпилировать текущий файл, который вы открыли в Emacs, используя M-x agda2-compile. Откроется другое окно с запросом Backend. Я использовал GHC в качестве входных данных, и он его скомпилировал. Да, и у меня есть ошибки, которые я не знаю, как исправить. Итак, я запросил поисковую систему и нашел:

module memo where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Foreign.Haskell using (Unit)

main : IO Unit
main = putStrLn (toCostring "Hello, Agda!")

Мне нужно указать, что первая строка module memo where должна совпадать с именем файла, которое в вашем случае - memo.agda.

person Compro Prasad    schedule 24.06.2018

arrow_upward
0
arrow_downward

Теперь на моей машине запущена программа hello world.

Следующий код компилируется и работает

open import Common.IO


main = putStrLn "Hello, world, strings working!"

это код, хранящийся в файле hello.agda, который я компилирую в emacs как hello. Я компилирую в emacs, выбирая agda > compile, параметр, который доступен в emacs при правильной установке agda.

Я не могу дать подробный учебник о том, как установить agda на emacs, поскольку мой друг сделал это за меня, но приведенный выше код работает и компилируется на emacs на linux, и эта настройка работает для меня.

person Adjam    schedule 26.03.2019