merge repositories

gen_graph.py

-#!/usr/bin/env python3
-
-import os
-
-def save(fn, z):
-    d = open(fn, 'w', encoding="utf-8")
-    d.write(z)
-    d.close()
-
-def main():
-
-    # MAIN
-    list_parse = []
-    dirs = ['Gen', 'Libs', 'ListsOp', 'Low', 'Mid']
-    for dir in dirs:
-        coqfiles = os.listdir(dir)
-        for coqfile in coqfiles:
-            if coqfile[-2:] == '.v':
-                list_parse.append(dir + '.' + coqfile[:-2])
-
-    requires = ''
-    prints = 'Print FileDependGraph \n'
-    for cq in list_parse:
-        requires += 'Require Import Tweetnacl.'+ cq + '.\n'
-        prints += '\t' + cq + '\n'
-
-    output = requires + '\n'
-    output += 'Require dpdgraph.dpdgraph.\n'
-    output += 'Set DependGraph File "main.dpd".\n'
-    output += prints + '.\n'
-    # print(list_parse)
-    print(output)
-    save('gen_graph_main.v', output)
-
-
-    # High
-    list_parse = []
-    dirs = ['High']
-    for dir in dirs:
-        coqfiles = os.listdir(dir)
-        for coqfile in coqfiles:
-            if coqfile[-2:] == '.v':
-                list_parse.append(dir + '.' + coqfile[:-2])
-    requires = ''
-    prints = 'Print FileDependGraph \n'
-    for cq in list_parse:
-        requires += 'Require Import Tweetnacl.'+ cq + '.\n'
-        prints += '\t' + cq + '\n'
-
-    output = requires + '\n'
-    output += 'Require dpdgraph.dpdgraph.\n'
-    output += 'Set DependGraph File "high.dpd".\n'
-    output += prints + '.\n'
-    # print(list_parse)
-    print(output)
-    save('gen_graph_high.v', output)
-
-
-if __name__ == '__main__':
-    main()

githelp

-echo "
-list of commands that you might want to know
-git add -A			: add all files
-git add --all			: add all files
-git add -u			: update modified files
-git commit -m <msg>		: commit some changes with <msg>
-git commit -am <msg>		: git add -u + git commit -m
-
-git mv <source> <destination>	: move a file/folder
-
-git status			: check local status
-git fetch			: check for changes online
-git pull			: check for changes online and update local
-git push			: push your commited changes online
-
-
-REVERT CHANGES :
-git checkout -- <file>		: reset your file/folder to the last commit
-git stash			: reset your local repo to the last commit
-
-git reset --hard                : complete reset to the last commit
-/!\ your changes will be destroyed
-
-
-IN CASE OF CONFLICT :
-git fetch --all
-git reset --hard origin/master
-/!\ your changes will be destroyed
-
-
-
-TO MERGE IN CASE OF CONFLICT : 
-git fetch			: parse the last modifications
-git difftool			: merge the files
-Edit the files (chose the right parts), commit and push.
-
-
-MORE ADVANCED STUFF :
-git stash save <message>	: save temporarly your changes and revert
-git stash list			: show the list of the previous \"stash\"
-git stash clear			: clear the previous list
-git stash pop			: return to your working state
-
-
-BRANCHES
-git checkout -b <branch name> : create a branch <branch name>
-git checkout <branch name> : switch to branch <branch name>
-git push -u --all
-
-git checkout <commit number> : switch to this commit /!\ DANGEROUS
-
-MERGE /!\ DANGEROUS
-git merge <branch name> merges ROOT BRANCH (the one you are on, see git status) with <branch name>.
-The changes are done on ROOT BRANCH.
-
-alias gtree='git log --oneline --decorate --all --graph'
-
-Add this to .git/config in order to have a nice output on ''git log''
-[log]
-	date = short
-[format]
-	pretty = format:%C(yellow)%h %>(10)%Cred%ad %<(13)%C(cyan)%an %Cgreen%d %Creset%s"

makefile

+all: coq-tweetnacl-spec coq-tweetnacl-vst
+
+
+coq-tweetnacl-spec:
+	cd proofs/spec ;\
+	./configure.sh ;\
+	$(MAKE) -j ;\
+	$(MAKE) install
+
+coq-tweetnacl-vst: coq-tweetnacl-spec
+	cd proofs/vst ;\
+	./configure.sh ;\
+	$(MAKE) -j ;\
+	$(MAKE) install

packages/coq-compcert/coq-compcert.3.2.0/opam

+opam-version: "2.0"
+maintainer: "Matej Kosik <matej.kosik@inria.fr>"
+homepage: "http://compcert.inria.fr/"
+license: "INRIA Non-Commercial License Agreement"
+build: [
+   ["./configure" "ia32-linux" {os = "linux"}
+    "ia32-macosx" {os = "darwin"}
+    "ia32-cygwin" {os = "cygwin"}
+    "-bindir" "%{bin}%"
+    "-libdir" "%{lib}%/coq/user-contrib/compcert"
+    "-clightgen"
+    "-ignore-coq-version"]
+   [make "-j%{jobs}%"]
+]
+install: [
+   [make "install"]
+]
+remove: [
+   ["rm" "%{bin}%/ccomp"]
+   ["rm" "%{bin}%/clightgen"]
+   ["rm" "%{share}%/compcert.ini"]
+   ["rm" "-R" "%{lib}%/coq/user-contrib/compcert"]
+]
+depends: [
+   "coq" {>= "8.7.0" & < "8.9"}
+   "menhir" {>= "20160303" & < "20180530"}
+]
+author: ["Xavier Leroy <xavier.leroy@inria.fr>"]
+description: """
+The CompCert C compiler.
+"""
+url {
+  src: "git+https://github.com/ildyria/CompCert.git#v3.2WithVO"
+}

packages/coq-dpdgraph/coq-dpdgraph.dev/opam

+opam-version: "2.0"
+maintainer: "Karmaki"
+homepage: "https://github.com/Karmaki/coq-dpdgraph"
+bug-reports: "https://github.com/Karmaki/coq-dpdgraph/issues"
+dev-repo: "git+https://github.com/Karmaki/coq-dpdgraph.git"
+license: "LGPL-2.1"
+authors: [
+  "Karmaki"
+]
+build: [
+  ["autoconf"]
+  ["./configure"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+remove: ["rm" "-R" "%{lib}%/coq/user-contrib/dpdgraph"]
+depends: [
+  "ocaml"
+  "coq" {>= "8.7" & < "8.9"}
+  "conf-autoconf"
+  "ocamlgraph"
+]
+description:"""
+Build dependency graphs between Coq objects, where Coq is the famous formal proof management system.
+
+The graph can be interpreted like this :
+edge n1 --> n2 : n1 uses n2
+node :
+green : proved lemma
+orange : axiom/admitted lemma
+dark pink : Definition, etc
+light pink : Parameter, etc
+violet : inductive,
+blue : constructor,
+multi-circled : not used (no predecessor in the graph)
+yellow box : module
+objects that are not in a yellow box are Coq objects.
+"""
+url {
+  src: "https://github.com/Karmaki/coq-dpdgraph/archive/v0.6.3.zip"
+}

packages/coq-reciprocity/coq-reciprocity.dev/opam

+opam-version: "2.0"
+maintainer: ""
+homepage: "https://github.com/Ekdohibs/coq-proofs"
+bug-reports: "https://github.com/Ekdohibs/coq-proofs/issues"
+dev-repo: "git+https://github.com/Ekdohibs/coq-proofs.git"
+license: "MIT"
+authors: [
+  "Nathanaël Courant"
+]
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Reciprocity"]
+depends: [
+  "coq" {>= "8.6.1" & < "8.9"}
+]
+description:"""
+Various proofs in Coq. As of now, only contains the proof of the theorem of quadratic reciprocity.
+"""
+url {
+  src: "git+https://github.com/ildyria/coq-proofs.git"
+}

packages/coq-ssr-elliptic-curves/coq-ssr-elliptic-curves.dev/opam

+opam-version: "2.0"
+maintainer: "pierre-yves@strub.nu"
+homepage: "https://github.com/strub/elliptic-curves-ssr"
+bug-reports: "https://github.com/strub/elliptic-curves-ssr/issues"
+dev-repo: "git+https://github.com/strub/elliptic-curves-ssr.git"
+license: "CeCILL-B"
+authors: [
+  "Evmorfia-Iro Bartzia"
+  "Pierre-Yves Strub"
+]
+build: [
+  [make "config"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+remove: ["rm" "-R" "%{lib}%/coq/user-contrib/SsrEllipticCurves"]
+depends: [
+  "ocaml"
+  "coq" {>= "8.7" & < "8.9"}
+  "coq-mathcomp-ssreflect"  {>= "1.6" & < "1.8"}
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-field"
+  "coq-mathcomp-multinomials"  {= "1.1"}
+]
+synopsis:
+  "A Formal Library about Elliptic Curves for the Mathematical Components Library."
+flags: light-uninstall
+url {
+  src: "git+https://github.com/strub/elliptic-curves-ssr.git#981ac368cddef9719e188101ae5068720771dd40"
+}

opam → packages/coq-tweetnacl-spec/coq-tweetnacl-spec.dev/opam

-opam-version: "1.2"
-name: "coq-tweetnacl"
-version: "dev"
+opam-version: "2.0"
+name: "coq-tweetnacl-spec"
 maintainer: "benoit@cs.ru.nl"
 homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
-bug-reports: "none"
-License: "MIT"
+license: "MIT"
 build: [
   ["./configure.sh"]
   [make "-j%{jobs}%"]
 ]
 install: [
-  ["mkdir" "-p" "%{lib}%/coq/user-contrib/Tweetnacl"]
-  ["cp" "-r" "Libs" "%{lib}%/coq/user-contrib/Tweetnacl/"]
-  ["cp" "-r" "ListsOp" "%{lib}%/coq/user-contrib/Tweetnacl/"]
-  ["cp" "-r" "Low" "%{lib}%/coq/user-contrib/Tweetnacl/"]
-  ["cp" "-r" "Mid" "%{lib}%/coq/user-contrib/Tweetnacl/"]
-  ["cp" "-r" "High" "%{lib}%/coq/user-contrib/Tweetnacl/"]
+  [make "install"]
 ]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Tweetnacl"]
 depends: [
-  "coq" {>= "8.7.0"}
-  "coq-coqprime" 
-  "coq-stdpp"
+  "coq" {>= "8.7.0" & < "8.9"}
+  "coq-coqprime" {= "1.0.3"}
+  "coq-stdpp" {= "1.1.0"}
   "coq-ssr-elliptic-curves"
-  "coq-mathcomp-ssreflect"
+  "coq-mathcomp-multinomials"
+  "coq-mathcomp-ssreflect" {= "1.7.0"}
+  "coq-reciprocity"
 ]
+author: [
+  "benoit@cs.ru.nl"
+  "timmy@timmyweerwag.nl"
+  ]
+description: """
+Model to verify Tweetnacl
+"""
+url {
+  src: "git+https://github.com/ildyria/coq-tweetnacl-verif/tree/master/proofs/spec"
+}

packages/coq-tweetnacl-verif/coq-tweetnacl-verif.dev/opam

+opam-version: "2.0"
+name: "coq-tweetnacl-verif"
+maintainer: "benoit@cs.ru.nl"
+homepage: "https://gitlab.science.ru.nl/benoit/Tweetnacl_verif/"
+license: "MIT"
+build: []
+install: [
+  [make "-j%{jobs}%"]
+]
+remove: []
+depends: [
+  "coq" {>= "8.7.0" & < "8.9"}
+  "coq-coqprime" {= "1.0.3"}
+  "coq-stdpp" {= "1.1.0"}
+  "coq-ssr-elliptic-curves"
+  "coq-mathcomp-multinomials"
+  "coq-mathcomp-ssreflect" {= "1.7.0"}
+  "coq-reciprocity"
+  "coq-vst" {= "2.0"}
+]
+author: [
+  "benoit@cs.ru.nl"
+  ]
+description: """
+Verifying the Tweetnacl implementation with VST
+"""
+url {
+  src: "git+https://github.com/ildyria/coq-tweetnacl-verif/"
+}

packages/coq-tweetnacl-vst/coq-tweetnacl-vst.dev/opam

+opam-version: "2.0"
+name: "coq-tweetnacl-vst"
+maintainer: "benoit@cs.ru.nl"
+homepage: "https://gitlab.science.ru.nl/benoit/Tweetnacl_verif/"
+license: "MIT"
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Tweetnacl_verif"]
+depends: [
+  "coq" {>= "8.7.0"}
+  "coq-coqprime"
+  "coq-stdpp"
+  "coq-ssr-elliptic-curves"
+  "coq-mathcomp-ssreflect"
+  "coq-vst" {= "2.0"}
+  "coq-tweetnacl-spec"
+]
+author: [
+  "benoit@cs.ru.nl"
+  ]
+description: """
+Verifying the Tweetnacl implementation with VST
+"""
+url {
+  src: "git+https://github.com/ildyria/coq-tweetnacl-verif/master/tree/proofs/vst"
+}

packages/coq-vst/coq-vst.2.0/opam

+opam-version: "2.0"
+maintainer: "VST team"
+homepage: "http://vst.cs.princeton.edu/"
+license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"
+build: [
+	[make "-j%{jobs}%" "COMPCERT=%{lib}%/coq/user-contrib/compcert" "version.vo" "msl" "veric" "floyd"]
+	]
+install: [
+	["mkdir" "-p" "%{lib}%/coq/user-contrib/VST"]
+	["cp" "-r" "msl" "%{lib}%/coq/user-contrib/VST/"]
+	["cp" "-r" "veric" "%{lib}%/coq/user-contrib/VST/"]
+	["cp" "-r" "floyd" "%{lib}%/coq/user-contrib/VST/"]
+	["cp" "-r" "sepcomp" "%{lib}%/coq/user-contrib/VST/"]
+	]
+remove: [
+	["rm" "-fr" "%{lib}%/coq/user-contrib/VST"]
+	]
+depends: [
+  "coq" {>= "8.7.0" & < "8.9"}
+  "coq-compcert" {>= "3.2" & < "3.3"}
+]
+tags: []
+authors: ["Andrew W. Appel"
+  "Lennart Beringer"
+  "Sandrine Blazy"
+  "Qinxiang Cao"
+  "Santiago Cuellar"
+  "Robert Dockins"
+  "Josiah Dodds"
+  "Nick Giannarakis"
+  "Samuel Gruetter"
+  "Aquinas Hobor"
+  "Jean-Marie Madiot"
+  ]
+description: """
+Verified Software Toolchain
+
+The software toolchain includes static analyzers to check assertions about your program;
+optimizing compilers to translate your program to machine language;
+operating systems and libraries to supply context for your program.
+The Verified Software Toolchain project assures with machine-checked
+proofs that the assertions claimed at the top of the toolchain really
+hold in the machine-language program, running in the operating-system context.
+"""
+url {
+  src: "git+https://github.com/ildyria/VST.git#v2.0_ssReflect_notation"
+}