| 1 |
719ae9fd
|
Lélio Brun
|
(lang dune 2.8)
|
| 2 |
d0f26f04
|
Lélio Brun
|
|
| 3 |
719ae9fd
|
Lélio Brun
|
(name lustrec)
|
| 4 |
|
|
(version 1.7)
|
| 5 |
|
|
|
| 6 |
|
|
(using dune_site 0.1)
|
| 7 |
|
|
(using menhir 2.0)
|
| 8 |
|
|
(generate_opam_files true)
|
| 9 |
|
|
|
| 10 |
|
|
(license LGPL)
|
| 11 |
|
|
(authors "Pierre-Loic Garoche <ploc@garoche.net>"
|
| 12 |
|
|
"Xavier Thirioux <thirioux@enseeiht.fr>")
|
| 13 |
|
|
(maintainers "Pierre-Loic Garoche <ploc@garoche.net>")
|
| 14 |
|
|
(source (uri git+https://cavale.enseeiht.fr/git/lustrec#unstable))
|
| 15 |
|
|
(bug_reports https://cavale.enseeiht.fr/redmine/projects/lustrec/issues)
|
| 16 |
|
|
(homepage https://cavale.enseeiht.fr/redmine/projects/lustrec/)
|
| 17 |
|
|
|
| 18 |
|
|
(package
|
| 19 |
|
|
(name lustrec)
|
| 20 |
|
|
(sites
|
| 21 |
|
|
(lib plugins)
|
| 22 |
57c96fb7
|
Lélio Brun
|
(lib verifiers)
|
| 23 |
|
|
(lib include_)
|
| 24 |
|
|
(share testgen))
|
| 25 |
719ae9fd
|
Lélio Brun
|
(synopsis "A Lustre compiler toolset")
|
| 26 |
|
|
(description
|
| 27 |
|
|
"lustrec is structured around the modular compilation scheme proposed by \
|
| 28 |
|
|
Biernacki, Colaço, Hamon, and Pouzet at LCTES'08. It is an open source \
|
| 29 |
|
|
lustre compiler that provides verification capabilities. It is currently \
|
| 30 |
|
|
mainly used through the CocoSim platform, a Matlab toolbox to perform V&V \
|
| 31 |
|
|
of Simulink models. Within CocoSim, the Lustre language is used as an \
|
| 32 |
|
|
intermediate representation and relies mainly on lustrec to produce code \
|
| 33 |
|
|
or verification artifacts.")
|
| 34 |
ca7e8027
|
Lélio Brun
|
(depends
|
| 35 |
97d4e95e
|
Lélio Brun
|
conf-gmp
|
| 36 |
ca7e8027
|
Lélio Brun
|
ocamlgraph
|
| 37 |
|
|
menhir
|
| 38 |
|
|
zarith
|
| 39 |
|
|
yojson
|
| 40 |
|
|
ppx_deriving_yojson
|
| 41 |
|
|
; cmdliner
|
| 42 |
|
|
dune-site)
|
| 43 |
|
|
(depopts z3))
|