(lang dune 3.8)
(using coq 0.8)

(generate_opam_files true)

(package
  (name coq-osiris)
  (authors
     "François Pottier"
     "Arnaud Daby-Seesaram"
     "Jean-Marie Madiot"
     "Remy Seassau"
     "Irene Yoon"
   )
  (maintainers
    "François Pottier"
  )
  (homepage https://gitlab.inria.fr/fpottier/osiris/)
  (bug_reports francois.pottier@inria.fr)
  (synopsis "An instance of the Iris verification framework for OCaml")
  (depends
     dune
     coq
     (coq-stdpp (= 1.9.0))
     (coq-iris  (= 4.1.0))
     coq-equations
  )
)

(package
  (name coq-osiris-examples)
  (authors
     "François Pottier"
     "Jean-Marie Madiot"
     "Remy Seassau"
     "Irene Yoon"
   )
  (maintainers
    "François Pottier"
  )
  (homepage https://gitlab.inria.fr/fpottier/osiris/)
  (bug_reports francois.pottier@inria.fr)
  (synopsis "Examples of use of Osiris")
  (depends
     dune
     coq-stdpp
     coq-iris
     coq-osiris
  )
)

(package
  (name osiris-interpreter)
  (authors "Jean-Marie Madiot")
  (maintainers "Jean-Marie Madiot")
  (homepage https://gitlab.inria.fr/fpottier/osiris/)
  (bug_reports jean-marie.madiot@inria.fr)
  (synopsis "Osiris Interpreter")
  (depends coq-osiris)
)