เรียกใช้แอป 'Hello World' ใน Agda emacs

ฉันติดตั้งคอมไพเลอร์ Agda แล้ว ไบนารี่ได้จากที่นี่: http://ocvs.cfv.jp/Agda/how-to-install-windows.html

... และฉันกำลังพยายามทำให้มันรวบรวมแอพ Hello World ง่ายๆ (ฉันพบรหัส 'Hello World' ของ Agda ออนไลน์)

แต่ฉันไม่เคยใช้ 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
นอกจากนี้ pieease ยังเปิดเผยสิ่งที่คุณทำเพื่อสร้างข้อความแสดงข้อผิดพลาดนี้ คุณพิมพ์คำสั่งเช่น 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 เป็นเพียง wrapper เพื่อเรียกใช้คำสั่งใด ๆ ที่พบใน 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