Merge pull request #7 from h0nzZik/dist-2

Vagrant, Dune, opam, doc

dist/vagrant/fedora39/Vagrantfile

@@ -0,0 +1,87 @@
+# -*- mode: ruby -*-
+# vi: set ft=ruby :
+
+# All Vagrant configuration is done below. The "2" in Vagrant.configure
+# configures the configuration version (we support older styles for
+# backwards compatibility). Please don't change it unless you know what
+# you're doing.
+Vagrant.configure("2") do |config|
+  # The most common configuration options are documented and commented below.
+  # For a complete reference, please see the online documentation at
+  # https://docs.vagrantup.com.
+
+  # Every Vagrant development environment requires a box. You can search for
+  # boxes at https://vagrantcloud.com/search.
+  config.vm.box = "generic/fedora39"
+
+  # Disable automatic box update checking. If you disable this, then
+  # boxes will only be checked for updates when the user runs
+  # `vagrant box outdated`. This is not recommended.
+  # config.vm.box_check_update = false
+
+  # Create a forwarded port mapping which allows access to a specific port
+  # within the machine from a port on the host machine. In the example below,
+  # accessing "localhost:8080" will access port 80 on the guest machine.
+  # NOTE: This will enable public access to the opened port
+  # config.vm.network "forwarded_port", guest: 80, host: 8080
+
+  # Create a forwarded port mapping which allows access to a specific port
+  # within the machine from a port on the host machine and only allow access
+  # via 127.0.0.1 to disable public access
+  # config.vm.network "forwarded_port", guest: 80, host: 8080, host_ip: "127.0.0.1"
+
+  # Create a private network, which allows host-only access to the machine
+  # using a specific IP.
+  # config.vm.network "private_network", ip: "192.168.33.10"
+
+  # Create a public network, which generally matched to bridged network.
+  # Bridged networks make the machine appear as another physical device on
+  # your network.
+  # config.vm.network "public_network"
+
+  # Share an additional folder to the guest VM. The first argument is
+  # the path on the host to the actual folder. The second argument is
+  # the path on the guest to mount the folder. And the optional third
+  # argument is a set of non-required options.
+  # config.vm.synced_folder "../data", "/vagrant_data"
+  config.vm.provision "file", source: "../../../minuska", destination: "$HOME/minuska-src"
+
+  # Disable the default share of the current code directory. Doing this
+  # provides improved isolation between the vagrant box and your host
+  # by making sure your Vagrantfile isn't accessible to the vagrant box.
+  # If you use this you may want to enable additional shared subfolders as
+  # shown above.
+  # config.vm.synced_folder ".", "/vagrant", disabled: true
+
+  # Provider-specific configuration so you can fine-tune various
+  # backing providers for Vagrant. These expose provider-specific options.
+  # Example for VirtualBox:
+  #
+  # config.vm.provider "virtualbox" do |vb|
+  #   # Display the VirtualBox GUI when booting the machine
+  #   vb.gui = true
+  #
+  #   # Customize the amount of memory on the VM:
+  #   vb.memory = "1024"
+  # end
+  #
+  # View the documentation for the provider you are using for more
+  # information on available options.
+
+  # Enable provisioning with a shell script. Additional provisioners such as
+  # Ansible, Chef, Docker, Puppet and Salt are also available. Please see the
+  # documentation for more information about their specific syntax and use.
+  config.vm.provision "shell", inline: <<-SHELL
+    dnf update
+    dnf install -y opam ocaml-dune
+  SHELL
+
+  config.vm.provision "shell", privileged: false, inline: <<-SHELL
+    opam init --auto-setup
+    eval $(opam env)
+    opam pin add coq 8.19.0
+    opam repo add coq-released https://coq.inria.fr/opam/released
+    opam install coq-equations coq-stdpp core core_unix menhir
+  SHELL
+
+end

doc/dependencies.md

@@ -17,6 +17,10 @@ However, to support building Minuska without Nix, we list the required dependenc
 - zarith
 
 
-[Here](../dist/vagrant) we WILL provide (TODO!) a Vagrant configuration for a [Ubuntu machine](../dist/vagrant/ubuntu2310)
-and [Fedora machine](../dist/vagrant/fedora38) with all the dependencies installed, once all the packages become available.
+[Here](../dist/vagrant) we provide a Vagrant configuration for:
+
+- a [Fedora machine](../dist/vagrant/fedora39)
+- a [Ubuntu machine](../dist/vagrant/ubuntu2310) (TODO)
+
+with all the dependencies installed.
 Inside the machines, the [`minuska` directory](../minuska) is mounted as `/minuska-src`.

minuska/coq-minuska.opam

@@ -0,0 +1,32 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "A formally verified programming language framework"
+description:
+  "Minuska is a programming language framework capable of generating interpreters from operational semantics."
+maintainer: ["Jan Tušil <[email protected]>"]
+authors: ["Jan Tušil <[email protected]>"]
+license: "MIT"
+tags: ["operational semantics" "interpreters"]
+homepage: "https://github.com/h0nzZik/minuska"
+bug-reports: "https://github.com/h0nzZik/minuska/issues"
+depends: [
+  "dune" {>= "3.14"}
+  "coq"
+  "menhir"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/h0nzZik/minuska.git"

minuska/dune-project

@@ -11,19 +11,18 @@
 (source
  (github h0nzZik/minuska))
 
-(authors "Jan Tušil")
+(authors "Jan Tušil <[email protected]>")
 
-(maintainers "Jan Tušil")
+(maintainers "Jan Tušil <[email protected]>")
 
-(license LICENSE)
-
-(documentation https://url/to/documentation)
+(license MIT)
 
 (package
  (name coq-minuska)
- (synopsis "A formally verified semantic framework")
- (description "A longer description")
+ (depends coq menhir)
+ (synopsis "A formally verified programming language framework")
+ (description "Minuska is a programming language framework capable of generating interpreters from operational semantics.")
  (tags
-  (topics "to describe" your project)))
+  ("operational semantics" interpreters)))
 
 ; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project