Getting started with jasmin
Install Jasmin (and EasyCrypt)
There are multiple ways to install the Jasmin compiler, the easiest is on Debian (or Debian-derived) systems via apt:
wget -qO- https://formosa-crypto.org/formosa-archive-keyring.pgp | gpg --dearmor > /etc/apt/trusted.gpg.d/formosa-crypto.gpg
echo 'deb [signed-by=/etc/apt/trusted.gpg.d/formosa-crypto.gpg] https://repo.formosa-crypto.org/debian trixie main' > /etc/apt/sources.list.d/formosa-crypto.list
sudo apt update
sudo apt install jasmin-compiler easycrypt libjasmin-easycrypt
echo 'deb [signed-by=/etc/apt/trusted.gpg.d/formosa-crypto.gpg] https://repo.formosa-crypto.org/debian trixie main' > /etc/apt/sources.list.d/formosa-crypto.list
sudo apt update
sudo apt install jasmin-compiler easycrypt libjasmin-easycrypt
For other options, including how to build developer versions from source, please see the Jasmin installation guide.
A first example
Install ProofGeneral (for vi users)
First install emacs:
sudo apt install emacs
Create a file ~/.emacs with the following content:
(setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3")
;; Set up package.el to work with MELPA
(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
;; (package-refresh-contents)
;; Download Evil
(unless (package-installed-p 'evil)
(package-install 'evil))
;; Enable Evil
(require 'evil)
(evil-mode 1)
(evil-define-key 'normal proof-mode-map (kbd "C-c RET") 'proof-goto-point)
(setq evil-want-abbrev-expand-on-insert-exit nil)
(require 'evil-tabs)
(global-evil-tabs-mode t)
(custom-set-variables
;; custom-set-variables was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
'(package-selected-packages '(proof-general evil-tabs evil)))
(custom-set-faces
;; custom-set-faces was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
)
Now start emacs and inside emacs run
;; Set up package.el to work with MELPA
(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
;; (package-refresh-contents)
;; Download Evil
(unless (package-installed-p 'evil)
(package-install 'evil))
;; Enable Evil
(require 'evil)
(evil-mode 1)
(evil-define-key 'normal proof-mode-map (kbd "C-c RET") 'proof-goto-point)
(setq evil-want-abbrev-expand-on-insert-exit nil)
(require 'evil-tabs)
(global-evil-tabs-mode t)
(custom-set-variables
;; custom-set-variables was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
'(package-selected-packages '(proof-general evil-tabs evil)))
(custom-set-faces
;; custom-set-faces was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
)
:package-refresh-contents
:package-install <ENTER>
proof-general
:package-install <ENTER>
proof-general