Menjalankan aplikasi 'Hello World' di Agda emacs

Saya memasang kompiler Agda, biner dapat dari sini: http://ocvs.cfv.jp/Agda/how-to-install-windows.html

... dan saya mencoba membuatnya mengkompilasi aplikasi hello world sederhana (saya menemukan kode Agda 'Hello World' online)

Namun saya belum pernah menggunakan Emacs sebelumnya, dan saya tidak tahu harus mulai dari mana, atau perintah mana yang digunakan untuk mengkompilasi dan menjalankannya. Saya baru mengenal Agda, yang tampaknya memiliki pilihan terbatas untuk kompiler, dan tidak memiliki tutorial langkah demi langkah. Di bawah ini adalah tangkapan layar kompiler Emacs dengan kode yang saya temukan:

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

module System.IO.Examples.HelloWorld where

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

Saya mencari petunjuk langkah demi langkah untuk menjalankan program sederhana 'Hello World'

Kompilator Agda Emacs

Contoh yang berfungsi dengan kompiler lain juga akan menjadi jawaban yang dapat diterima

Terima kasih!


emacs agda
person Adjam    schedule 18.06.2018    source sumber
comment
Sudahkah Anda membaca dokumen?   -  person user2407038    schedule 20.06.2018
comment
Saya sudah melakukannya sekarang, tetapi saya memerlukan panduan dasar langkah demi langkah   -  person Adjam    schedule 21.06.2018
comment
Harap edit pertanyaan Anda untuk menyertakan pesan kesalahan sebagai teks sehingga kami dapat menyalin/menempelkannya dan agar Google dapat menemukannya .   -  person tripleee    schedule 21.06.2018
comment
Juga harap ungkapkan apa yang sebenarnya Anda lakukan hingga menghasilkan pesan kesalahan ini. Apakah Anda mengetikkan perintah seperti M-x compile atau apakah Anda menggunakan urutan penekanan tombol seperti C-c C-c?   -  person tripleee    schedule 21.06.2018

Jawaban (3)


arrow_upward
0
arrow_downward

Sepertinya Anda mencoba sesuatu seperti M-x compile umum daripada fungsi Agda tertentu.

Indikator mode Agda:run di baris mode Emacs menunjukkan bahwa Anda menjalankan proses Agda di buffer lain, tetapi Anda tidak melihatnya. Mode Agda mungkin memiliki sesuatu seperti agda-eval-buffer yang akan meneruskan program Anda saat ini ke proses tersebut, dan menampilkan hasilnya di bagian bawah panel. (Coba beralih ke buffer bernama *inferior-agda* secara manual jika Anda tidak dapat mencapai buffer tersebut dengan cara lain.)

Situs yang Anda tautkan mengatakan itu Agda 1 dan Anda mungkin harus mencari Agda 2 di situs lain.

Di bawah ini adalah jawaban asli saya, yang mungkin masih memberikan beberapa wawasan bermanfaat.

Pesan kesalahan menunjukkan bahwa Anda perlu menginstal make.

Saya kira mungkin ada ketergantungan tambahan yang hilang setelah Anda memperbaikinya. Idealnya, dokumentasi harus secara eksplisit menentukan apa yang perlu Anda instal.

make hanyalah pembungkus untuk menjalankan perintah apa pun yang ditemukan di Makefile lokal. Jika tidak ada file seperti itu, Anda mungkin ingin mengubah perintah kompilasi ke yang lain. (Biasanya Emacs meminta Anda untuk menjalankan perintah, tetapi menyediakan default yang masuk akal.)

person tripleee    schedule 21.06.2018

arrow_upward
0
arrow_downward

Mengingat saya menggunakan Linux dan bukan ahli agda, solusi ini mungkin tidak sepadan. Tapi tetap saja saya akan mencobanya.

Ketika saya menginstal agda dan agda-stdlib di sistem saya, itu memberi saya file bernama agda2.el di /usr/share/agda/emacs-mode. Artinya, saya baru saja memiliki yang berikut ini di file ~/.emacs.d/init.el saya:

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

Karena Anda sudah memiliki pengaturan mode agada di Emacs, hal di atas tidak akan berguna kecuali versi mode agda Anda sudah lama.

Kami dapat mengkompilasi file yang Anda buka saat ini di Emacs menggunakan M-x agda2-compile. Melakukan hal ini akan membuka prompt lain yang meminta Anda untuk Backend. Saya menggunakan GHC sebagai input dan mengkompilasinya. Ya, dan saya mendapat beberapa kesalahan yang saya tidak tahu cara memperbaikinya. Jadi, saya bertanya di mesin pencari dan menemukan:

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!")

Saya perlu menunjukkan bahwa baris pertama module memo where harus sama dengan nama file yang untuk kasus Anda adalah memo.agda.

person Compro Prasad    schedule 24.06.2018

arrow_upward
0
arrow_downward

Saya sekarang menjalankan program hello world di mesin saya.

Kode berikut dikompilasi dan berfungsi

open import Common.IO


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

adalah kodenya, disimpan dalam file 'hello.agda', yang saya kompilasi di emacs menjadi 'hello'. Saya mengkompilasi di emacs dengan memilih agda > compile, opsi yang tersedia di emacs ketika agda diinstal dengan benar.

Saya tidak bisa memberikan tutorial mendetail tentang cara menginstal agda di emacs seperti yang dilakukan teman untuk saya, tetapi kode di atas berfungsi, dan dikompilasi di emacs di linux, yang merupakan pengaturan yang berfungsi untuk saya.

person Adjam    schedule 26.03.2019