Commit 2ee10bbb authored by François Bobot's avatar François Bobot
Browse files

Add dune-project and farith.opam

parent aae1113b
......@@ -42,4 +42,5 @@ native_compute_profile_*.data
time-of-build-after.log
time-of-build-before.log
time-of-build-both.log
time-of-build-pretty.log
\ No newline at end of file
time-of-build-pretty.log
/_build/
include CoqMakefile
all:
dune build --root=$$(pwd) @install farith.opam
CoqMakefile:
@ coq_makefile -f _CoqProject -o CoqMakefile
test:
dune runtest --root=$$(pwd)
.PHONY: cleandoc doc
cleandoc:
@ rm -rf doc/
doc:
@ mkdir -p doc
@ cd thry && coq2html -base F -d ../doc *.v *.glob
\ No newline at end of file
promote:
dune promote --root=$$(pwd)
(library
(name farith2)
(public_name farith2)
(name farith)
(public_name farith)
(libraries zarith base)
(preprocess
(pps ppx_deriving.std ppx_hash))
......
(lang dune 3.0)
(generate_opam_files true)
(using coq 0.3)
(name farith)
(package
(name farith)
(synopsis "formaly verified floating-points valuations based on Flocq")
(maintainers "François Bobot")
(authors "François Bobot" "Loïc Correnson" "Arthur Correnson")
(depends zarith base ppx_deriving ppx_hash)
)
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
synopsis: "formaly verified floating-points valuations based on Flocq"
depends: [
"dune" {>= "3.0"}
"zarith"
"base"
"ppx_deriving"
"ppx_hash"
"odoc" {with-doc}
]
build: [
["dune" "subst"] {dev}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment