Skip to content

Latest commit

 

History

History
107 lines (76 loc) · 9.95 KB

INSTALL.md

File metadata and controls

107 lines (76 loc) · 9.95 KB

Οδηγίες Εγκατάστασης του Coq Proof Assistant

TL;DR Εγκατάσταση του Coq μέσω opam και του VSCoq extension για VS Code.

Προκειμένου να κάνετε τις εργασίες του μαθήματος, θα χρειαστείτε εγκατεστημένο το Coq Proof Assistant (version >= 8.18.0), καθώς και ένα IDE με υποστήριξη για Coq. Το Coq είναι διαθέσιμο για Linux, MacOS και Windows.

Coq Installation

Linux και MacOS

Installation with Opam (για έμπειρους - recommended)

Το Coq μπορεί να εγκατασταθεί μέσω του opam, του package manager της OCaml. Οι παρακάτω οδηγίες είναι μεταφρασμένες από εδώ.

  • Εγκαταστήστε την OCaml και το opam από εδώ.
  • Σε περίπτωση που έχετε το opam ήδη εγκατεστημένο, βεβαιωθείτε ότι έχετε έκδοση >= 2.1.0.
# Make sure opam version is 2.1.0 or above.
opam --version
  • Μετά την εγκατάσταση, αρχικοποιήστε το opam με τις ακόλουθες εντολές. Η εντολή opam init θα σας ζητήσει να επιτρέψετε στο opam να ρυθμίσει τα script αρχικοποίησης, το οποίο καλό θα είναι να αποδεχτείτε προκειμένου να μην χρειάζεται να αρχικοποιείτε το opam σε κάθε νέο shell.
opam init
eval $(opam env)
  • Για να εγκαταστήσετε το Coq, εκτελέστε την παρακάτω εντολή. (Η εκτέλεση θα διαρκέσει αρκετά λεπτά καθώς χτίζει τα sources του Coq):
# Pin the coq package to version 8.20.0 and install it.
opam pin add coq 8.20.0
  • Βεβαιωθείτε ότι το Coq έχει εγκατασταθεί. Η παρακάτω εντολή θα πρέπει να εκτελείται, τυπώνοντας την έκδοση που μόλις εγκαταστήσατε.
coqc -v

Binary Installation (για αρχάριους)

Αυτή η μέθοδος εγκατάστασης δεν προτείνεται, εκτός και εάν έχετε σημαντικά προβλήματα εγκατάστασης με τις άλλες μεθόδους. Μπορείτε να κατεβάσετε ένα από τα binary distributions που βρίσκονται εδώ.

Windows

Binary Installation

Μπορείτε να εγκαταστήσετε το Coq χρησιμοποιώντας τον Windows installer που θα βρείτε εδώ. Αυτό θα εγκαταστήσει και το CoqIDE που παρέχει ένα διαδραστικό περιβάλλον χρήσης του Coq Proof Assistant. Παρότι υποβέλτιστη, αυτή η λύση θα σας καλύψει για τις ανάγκες του μαθήματος.

Για να ελέγξετε την εγκατάσταση σας, ανοίξτε το CoqIDE και στη συνέχεια την διάλεξη intro.v. Θα πρέπει να μπορείτε να

Installation Using WSL

Εάν χρησιμοποιείτε WSL (Windows Subsystem for Linux), μπορείτε να εγκαταστήσετε το Coq ακολουθώντας τις οδηγίες για Linux.

Editors

Προκειμένου να χρησιμοποιήσετε το Coq διαδραστικά, θα χρειαστείτε έναν IDE με υποστήριξη για Coq.

Visual Studio Code (recommended)

Η προτεινόμενη μέθοδος επεξεργασίας αρχείων Coq είναι μέσω του VSCoq extension του VS Code.

  • Εγκαταστήστε το VS Code από εδώ.
  • Eγκαταστήστε το Coq LSP
opam install vscoq-language-server
  • Ελέγξτε ότι η παραπάνω εγκατάσταση ήταν επιτυχής:
which vscoqtop

Η παραπάνω εντολή θα πρέπει να επιστρέφει το path του εκτελέσιμου αρχείου που εγκαταστήσατε.

  • Εγκαταστήστε την επέκταση VsCoq για το VS Code:

    • Ανοίξτε το VS Code.
    • Πατήστε F1 να ανοίξετε το command palette, πληκτρολογήστε Extensions: Install Extension και πατήστε enter.
    • Στον extension manager, αναζητήστε VsCoq και πατήστε enter ώστε να ανοίξετε το tab του VsCoq.
    • Στο tab του VsCoq πατήστε install.
    • Μετά την εγκατάσταση, πηγαίνετε στο extension settings, που θα βρείτε πατώντας το σύμβολο με το γρανάζι. Στο πεδίο Vscoq: Path εισάγετε το πλήρες μονοπάτι που επέστρεψε η εντολή which vscoqtop.

  • Θα πρέπει να μπορείτε τώρα να ανοίξετε και να επεξεργαστείτε διαδραστικά ένα αρχείο Coq. Ανοίξτε την εισαγωγική διάλεξη intro.v για να βεβαιωθείτε ότι η εγκατάσταση ήταν επιτυχής. Μπορείτε να χρησιμοποιήσετε τα βέλη που βρίσκονται δεξιά από το όνομα του αρχείου για να εκτελείτε βήμα-βήμα τις εντολές στο Coq. Αυτό σας επιτρέπει να εκτελείτε κάθε εντολή διαδραστικά και να παρακολουθείτε πώς εξελίσσεται η απόδειξή σας. Όταν βρίσκεστε σε proof mode, η κατάσταση της απόδειξής σας φαίνεται σε ένα βοηθητικό με το όνομα Coq Goals.

Tips:

  • Είναι χρήσιμο να εξοικειωθείτε με τα key bindings. Πηγαίνοντας στο Code > Preferences > Keyboard Shortcuts (ή πληκτρολογώντας Keyboard Shortcuts στο control palette (F1)) και ψάχνοντας για Coq: βλέπετε τα διαθέσιμα key bindings του VSCoq. Ιδιαίτερα χρήσιμα είναι τα step forward και step backward. Μπορείτε να τα αλλάξετε σε κάτι που να σας βολεύει (π.χ. control+up για step forward και control+down για step backwards).

  • Εάν σας βολεύει, μπορείτε να εγκαταστήσετε το extension Proof General keybindings for VSCoq, το οποίο παρέχει key bindings όμοια με αυτά του Proof General IDE για τον emacs (π.χ. control+c control+n για step forward και control+c control+u για step backward).

  • Στο activity bar (που βρίσκεται, by default, στα δεξιά) μπορείτε να πατήσετε το σύμβολο του Coq Proof Assistant προκειμένου να ανοίξετε το query panel. Αυτό σας επιτρέπει να εκτελέσετε διάφορα queries προκειμένου να αναζητήσετε θεωρήματα ή να δείτε τους τύπους και τους ορισμούς συμβόλων, όπως θα δούμε και στο μάθημα.

Emacs

  • Μπορείτε να κατεβάσετε τον emacs editor από εδώ.

  • Προκειμένου να έχετε IDE για Coq θα χρειαστείτε τον Proof General. Ακολουθήστε τις οδηγίες εγκατάστασης στην ενότητα Quick Installation.

Tips:

  • Το αρχείο .emacs τοποθετείται στο home directory σας.

  • Η συντόμευση M-x σημαίνει Alt-x (Linux + Windows) Opt-x (MacOS). Γενικότερα, το "META key" του emacs συμβολίζεται με M και αντιστοιχεί στο Alt ή Option αναλόγως με το σύστημα σας. M- σημαίνει κρατήστε πατημένο το πλήκτρο META ενώ πληκτρολογείτε. Αντίστοιχα, το σύμβολο C αντιστοιχεί στο πλήκτρο Control.

  • Υπάρχουν πολλά emacs tutorials online. Για παράδειγμα, δείτε εδώ και εδώ.

  • Θα βρείτε χρήσιμα τα Proof General key bindings που περιγράφονται εδώ και εδώ. Ιδιαίτερα χρήσιμα είναι τα:

    • C-c C-n: step forward
    • C-c C-u: step backward
    • C-c C-RET: go to point
    • C-c C-b: go to end of file

Vim

Εάν χρησιμοποιείτε Vim μπορείτε να εγκαταστήσετε το plugin Coqtail.

CoqIDE

Τα binary installations του Coq έρχονται μαζί με τον CoqIDE που είναι ένα περιβάλλον για διαδραστικές αποδείξεις με Coq. Μπορείτε να βρείτε περισσότερες πληροφορίες εδώ