From 719ae9fda4f32ba088b950fb9932e7da401d6b3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Wed, 3 Feb 2021 14:47:35 +0100
Subject: [PATCH] migration draft on dune
---
.gitignore | 6 +-
.gitlab-ci.yml | 346 ++++++++++++++++++
.merlin | 43 ---
README.md | 18 +-
dune-project | 32 ++
lustrec.opam | 33 ++
opam | 44 ---
src/.merlin | 1 -
src/arrow.ml | 2 +-
src/arrow.mli | 2 +-
src/backends/.merlin | 1 -
src/backends/Ada/.merlin | 1 -
src/backends/C/.merlin | 1 -
src/backends/C/c_backend_header.ml | 4 +-
src/backends/EMF/.merlin | 1 -
src/backends/Horn/.merlin | 1 -
src/backends/Java/.merlin | 1 -
src/checks/.merlin | 1 -
src/checks/liveness.ml | 1 -
src/dune | 128 +++++++
src/features/.merlin | 1 -
src/features/machine_types/.merlin | 1 -
src/machine_code.ml | 4 +-
src/ocaml_utils.ml.in | 1 -
src/options_management.ml | 3 +-
src/parsers/.merlin | 1 -
src/parsers/dune | 12 +
src/parsers/parse.ml | 2 -
src/pluginList.ml.in | 5 -
src/plugins/.merlin | 1 -
src/plugins/mpfr/.merlin | 1 -
src/plugins/pluginList.ml | 3 +
src/{ => plugins}/pluginType.ml | 0
src/{ => plugins}/plugins.ml | 13 +-
src/plugins/salsa/.merlin | 1 -
src/plugins/salsa/dune | 13 +
src/plugins/salsa/salsa_plugin.ml | 4 +
src/plugins/scopes/.merlin | 1 -
src/plugins/scopes/dune | 11 +
src/plugins/scopes/scopes.ml | 5 +-
src/tools/.merlin | 1 -
src/tools/seal/dune | 13 +
src/tools/seal/seal_verifier.ml | 3 +
src/tools/stateflow/.merlin | 1 -
src/tools/stateflow/common/.merlin | 1 -
src/tools/stateflow/json-parser/.merlin | 1 -
src/tools/stateflow/models/.merlin | 1 -
src/tools/stateflow/semantics/.merlin | 1 -
.../stateflow/semantics/cPS_evaluator.ml | 2 +-
src/tools/tiny/dune | 13 +
src/tools/tiny/tiny_verifier.ml | 5 +-
src/tools/zustre/dune | 15 +
src/tools/zustre/zustre_verifier.ml | 7 +-
src/utils/.merlin | 1 -
src/{ => utils}/dimension.ml | 0
src/utils/dune | 18 +
src/{ => utils}/location.ml | 0
src/utils/ocaml_utils.ml.ge403 | 1 +
src/utils/ocaml_utils.ml.lt403 | 1 +
src/utils/utils.ml | 1 -
src/verifierList.ml | 8 +
src/verifierList.ml.in | 6 -
src/verifiers.ml | 8 +-
src/{version.ml.in => version.ml} | 1 -
64 files changed, 704 insertions(+), 155 deletions(-)
create mode 100644 .gitlab-ci.yml
delete mode 100644 .merlin
create mode 100644 dune-project
create mode 100644 lustrec.opam
delete mode 100644 opam
delete mode 100644 src/.merlin
delete mode 100644 src/backends/.merlin
delete mode 100644 src/backends/Ada/.merlin
delete mode 100644 src/backends/C/.merlin
delete mode 100644 src/backends/EMF/.merlin
delete mode 100644 src/backends/Horn/.merlin
delete mode 100644 src/backends/Java/.merlin
delete mode 100644 src/checks/.merlin
create mode 100644 src/dune
delete mode 100644 src/features/.merlin
delete mode 100644 src/features/machine_types/.merlin
delete mode 100644 src/ocaml_utils.ml.in
delete mode 100644 src/parsers/.merlin
create mode 100644 src/parsers/dune
delete mode 100644 src/pluginList.ml.in
delete mode 100644 src/plugins/.merlin
delete mode 100644 src/plugins/mpfr/.merlin
create mode 100644 src/plugins/pluginList.ml
rename src/{ => plugins}/pluginType.ml (100%)
rename src/{ => plugins}/plugins.ml (85%)
delete mode 100644 src/plugins/salsa/.merlin
create mode 100644 src/plugins/salsa/dune
delete mode 100644 src/plugins/scopes/.merlin
create mode 100644 src/plugins/scopes/dune
delete mode 100644 src/tools/.merlin
create mode 100644 src/tools/seal/dune
delete mode 100644 src/tools/stateflow/.merlin
delete mode 100644 src/tools/stateflow/common/.merlin
delete mode 100644 src/tools/stateflow/json-parser/.merlin
delete mode 100644 src/tools/stateflow/models/.merlin
delete mode 100644 src/tools/stateflow/semantics/.merlin
create mode 100644 src/tools/tiny/dune
create mode 100644 src/tools/zustre/dune
delete mode 100644 src/utils/.merlin
rename src/{ => utils}/dimension.ml (100%)
create mode 100644 src/utils/dune
rename src/{ => utils}/location.ml (100%)
create mode 100644 src/utils/ocaml_utils.ml.ge403
create mode 100644 src/utils/ocaml_utils.ml.lt403
create mode 100644 src/verifierList.ml
delete mode 100644 src/verifierList.ml.in
rename src/{version.ml.in => version.ml} (99%)
diff --git a/.gitignore b/.gitignore
index 2174e4d2..938cbaf4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,10 +1,8 @@
*~
+_build/
/src/_build/
/setup.data
/setup.log
-/src/version.ml
-/src/pluginList.ml
-/myocamlbuild.ml
*.cmt
*.log
Makefile
@@ -12,4 +10,4 @@ Makefile
/src/_tags
/bin
*cache/
-/config.status
\ No newline at end of file
+/config.status
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
new file mode 100644
index 00000000..76c05842
--- /dev/null
+++ b/.gitlab-ci.yml
@@ -0,0 +1,346 @@
+# This reusable CI script is licensed under the MIT license.
+# See the complete license text at the end.
+
+### Configuration section
+
+# The versions of the compiler to test the project against.
+.build-matrix:
+ parallel:
+ # https://docs.gitlab.com/ee/ci/yaml/README.html#parallel-matrix-jobs
+ matrix:
+ # - OCAML_COMPILER: "4.00.1"
+ # - OCAML_COMPILER: "4.01.0"
+ # - OCAML_COMPILER: "4.02.1"
+ # - OCAML_COMPILER: "4.02.3"
+ # - OCAML_COMPILER: "4.03.0"
+ # - OCAML_COMPILER: "4.04.2"
+ # - OCAML_COMPILER: "4.05.0"
+ # - OCAML_COMPILER: "4.06.1"
+ # - OCAML_COMPILER: "4.07.1"
+ # - OCAML_COMPILER: "4.08.1"
+ # - OCAML_COMPILER: "4.09.1"
+ # - OCAML_COMPILER: "4.10.0"
+ - OCAML_COMPILER: "4.11.1"
+
+variables:
+ CLEAN_OPAM_CACHE: "false"
+ CLEAN_DUNE_CACHE: "false"
+ # If CLEAN_OPAM_CACHE is set to "true", the opam switch from previous CI jobs
+ # will not be reused.
+ # If CLEAN_DUNE_CACHE is set to "true", the dune _build directory
+ # from previous CI jobs will not be reused.
+
+ # In particular, you can run a manual pipeline
+ # with either variable set to "true" to purge a faulty cache.
+
+ # To run a manual gitlab pipeline, on your project go to
+ # "CI/CD" > pipelines, click "Run pipeline", the interface
+ # then offers to override variables, so you can change the
+ # value of any variable defined here.
+
+ DUNE_BUILD_TARGETS: "@all"
+ DUNE_TEST_TARGETS: "@runtest"
+ DUNE_DOC_TARGETS: "@doc"
+ # If you make one of these variables empty (: ""),
+ # the corresponding build step will be skipped.
+ # Setting them to other values can refine the build
+ # process, for example "@foo/runtest @bar/runtest" would only
+ # run the tests inside directories 'foo/' and 'bar/'
+ # (see Dune documentation on target aliases).
+
+
+# This CI script is written to be portable across projects.
+# None of the code below hardcodes project filenames,
+# OCaml versions or other project-specific details.
+#
+# If you want to add new behavior for your project, we recommend
+# trying to factorize it with project-agnostic code below,
+# and project-specific or manually-overridable choices in the
+# 'variables' section above.
+
+
+### Hacking advice
+#
+# Reference documentation for Gitlab CI configuration files:
+# https://docs.gitlab.com/ee/ci/yaml/
+#
+# If you edit this file and make syntax errors, the default
+# error messages will not help you, but Gitlab offers a "CI Lint"
+# service that provides very nice error messages:
+# https://docs.gitlab.com/ee/ci/lint.html
+#
+# To use this linter, go to "CI/CD > Pipelines", click the "CI Lint"
+# button in the top right, copy-paste your .gitlab-ci.yml file in
+# the form and click "Validate".
+#
+# We recommend systematically using the CI Lint whenever you change
+# this file, it can save you from wasted time and frustration.
+
+
+### Stages
+
+stages:
+ - build # build the project and run its tests
+ - deploy # deploys a website to Pages from the 'pages' branch
+
+
+### Build stage
+#
+# build the project and run its tests
+
+build:
+ stage: build
+
+ extends: .build-matrix # defines OCAML_COMPILER
+
+ variables:
+ ARTIFACTS: "artifacts/$OCAML_COMPILER"
+ # a local shortcut for the per-compiler artifact repository
+
+ FF_USE_FASTZIP: "true"
+ # A workaround against a bug in gitlab-runner's default
+ # unzipping implementation, which partially breaks caching for the dune _build cache.
+ # See https://gitlab.com/gitlab-org/gitlab-runner/-/issues/27496 for more details.
+
+ artifacts:
+ paths:
+ - artifacts/$OCAML_COMPILER
+
+ # run this job only if a 'dune-project' file exists;
+ # (In particular, this will not run in your "pages" branch
+ # if it does not itself use Dune.)
+ rules:
+ # https://docs.gitlab.com/ee/ci/yaml/#rules
+ - exists:
+ - dune-project
+
+ # This CI script uses a local switch, so we don't need
+ # a docker image with a pre-installed OCaml version, just opam.
+ # See https://hub.docker.com/r/ocaml/opam/ for other images.
+ image: ocaml/opam:debian-testing-opam
+
+ # We use a local opam switch in `./_opam` that is cached
+ # by Gitlab, and reused across all branches and pull requests.
+ cache:
+ # https://docs.gitlab.com/ee/ci/yaml/#cache
+ key: $OCAML_COMPILER
+ # keep a distinct cache for each compiler version
+ paths:
+ - _opam
+ # Reusing the same opam environment over a long time might result into
+ # unnatural choice of dependencies: repeatedly installing and updating
+ # dependencies may result in a different solver choices than doing
+ # a fresh setup.
+ #
+ # You can manually clean the _opam cache by running a manual pipeline
+ # with the variable CLEAN_OPAM_CACHE set to "true".
+
+ - _build
+ # You can manually clean the dune _build cache by running a manual pipeline
+ # with the variable CLEAN_DUNE_CACHE set to "true".
+
+ script:
+ - if [ "$CLEAN_OPAM_CACHE" == "true" ]; then echo "we clean the _opam cache as explicitly requested"; rm -fR _opam; fi
+ - if [ "$CLEAN_DUNE_CACHE" == "true" ]; then echo "we clean the dune _build cache as explicitly requested"; rm -fR _build; fi
+ # Note: Gitlab supports multi-line scripts with "- |" or "- >", but the
+ # display in the logs does not show the whole script being run, reducing
+ # understandability. We only use multi-line scripts for "echo" line,
+ # and otherwise keep long one-liners.
+ # https://docs.gitlab.com/ee/ci/yaml/script.html#split-long-commands
+
+ # see https://docs.gitlab.com/ee/ci/jobs/index.html#custom-collapsible-sections
+ # to understand the "section_{start,end}:`date +%s`:<name>\r\e[0K human-readable text" pattern
+ - echo -e "section_start:`date +%s`:setup_switch\r\e[0K setup opam switch"
+ - if [ -d _opam ]; then echo "we reuse the local opam switch from the CI cache"; fi
+
+ - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . $OCAML_COMPILER; fi
+ # --no-install prevents installing the package or its dependencies.
+ # we want to setup the external dependencies (depext) first, see below.
+ - echo -e "section_end:`date +%s`:setup_switch\r\e[0K"
+
+ - echo -e "section_start:`date +%s`:setup_deps\r\e[0K setup the package dependencies"
+ # (Note: when opam 2.1 will be available with native depext integration,
+ # the complex dance below will be replaceable by just
+ # opam install . --deps-only --locked --with-test --with-doc --yes
+ # which should start by installing depexts
+ # (possibly we will need to set some explicit environment variable first).
+ - opam install depext --yes
+ - opam install . --dry-run --deps-only --locked --with-test --with-doc --yes | awk '/-> installed/{print $3}' | xargs opam depext -iy
+ # the magical command above comes from https://github.com/ocaml/opam/issues/3790
+ # it installs both external dependencies and opam dependencies
+ - echo "(we used --locked to honor any lockfiles if present)"
+ - echo -e "section_end:`date +%s`:setup_deps\r\e[0K"
+
+ - echo -e "section_start:`date +%s`:project_build\r\e[0K build the project"
+ - eval $(opam env)
+ - if [ "$DUNE_BUILD_TARGETS" != "" ]; then dune build $DUNE_BUILD_TARGETS --display short; else echo "skipped (DUNE_BUILD_TARGETS is empty)"; fi
+ - echo -e "section_end:`date +%s`:project_build\r\e[0K"
+
+ - echo -e "section_start:`date +%s`:project_tests\r\e[0K run the tests"
+ - if [ "$DUNE_TEST_TARGETS" != "" ]; then dune build $DUNE_TEST_TARGETS --display short; else echo "skipped (DUNE_TEST_TARGETS is empty)"; fi
+ - echo -e "section_end:`date +%s`:project_tests\r\e[0K"
+
+ - echo -e "section_start:`date +%s`:project_doc\r\e[0K build the documentation"
+ - if [ "$DUNE_DOC_TARGETS" != "" ]; then dune build $DUNE_DOC_TARGETS --display short; else echo "skipped (DUNE_DOC_TARGETS is empty)"; fi
+ - echo -e "section_end:`date +%s`:project_doc\r\e[0K"
+
+ - echo -e "section_start:`date +%s`:artifacts\r\e[0K populating the artifacts"
+ - mkdir -p $ARTIFACTS
+ - >
+ echo "Build artifacts will be available at
+ $CI_JOB_URL/artifacts/browse/$ARTIFACTS
+ Note: by default Gitlab only keeps them for a few weeks."
+ - >
+ if [ "Dune_DOC_TARGETS" != "" ]; then
+ cp -r _build/default/_doc/_html $ARTIFACTS/doc;
+ echo "Documentation:
+ $CI_JOB_URL/artifacts/browse/$ARTIFACTS/doc/index.html";
+ fi
+ - >
+ if [ -f _build/log ];
+ then
+ mkdir -p $ARTIFACTS/_build;
+ cp _build/log $ARTIFACTS/_build/log
+ echo "Dune build log:
+ $CI_JOB_URL/artifacts/browse/$ARTIFACTS/_build/log";
+ fi
+ - echo -e "section_end:`date +%s`:artifacts\r\e[0K"
+
+
+### CI performance
+
+# Performance analysis of one 'build' job on a small, simple library project
+# (the project build/test/doc time is basically neglectible) on gitlab.com:
+#
+# (To get those numbers for your project, just look at a passing build and fold all
+# log sections.)
+#
+# 2m total
+# 56s preparing the docker image and CI environment
+# 14s restoring the _opam cache
+# 10s installing the project dependencies
+# (external dependencies are not cached, opam dependencies are cached)
+# 3s project build, tests, doc
+# 31s saving the _opam cache
+# 6s uploading artifacts
+#
+# When running with CLEAN_OPAM_CACHE=true, the costs are similar, except for
+# 7m30s building the local opam switch
+# 2m07s building the project dependencies (external and opam)
+# This shows that caching the local _opam switch is very important, as
+# its setup time dominates the build (for a small project).
+#
+# Another thing that is clear from these numbers is that splitting
+# your CI in several jobs could be fairly expensive: for each job you
+# pay 56s seconds of docker setup, plus 14s to restore the _opam
+# cache. (The 31s to save the cache afterwards can be avoided by using
+# a "policy: pull" setting if the job uses the _opam in a read-only
+# way.)
+#
+# This is why this CI script does everything in a single 'build' step.
+
+
+### Deploy stage
+#
+# pushing some project artifacts to the web.
+
+# The "pages" rule uploads a custom website whenever someones
+# pushes a commit to the "pages" branch of the repository.
+#
+# The content of the website is the sub-filesystem
+# located in the "docs/" subdirectory of the branch index.
+#
+# This behavior emulates the way per-repository Github pages work.
+#
+# If the repository is at
+# https://gitlab.com/<group>/<project>,
+# then the published website will be at
+# https://<group>.gitlab.io/<project>
+# In general see
+# https://docs.gitlab.com/ee/user/project/pages/getting_started_part_one.html#gitlab-pages-default-domain-names
+#
+# We previously used a setup where the documentation was pushed to
+# Gitlab Pages automatically when pushing a tag (a new release). This
+# was much less flexible, with no easy way for users to publish web
+# content *other* than the documentation, or to control when the
+# content should be refreshed.
+#
+# It is fairly simple to publish the documentation
+# from any branch with the current interface.
+# Here is an example script:
+#
+# # compute the current commit hash and branch name
+# git rev-parse --short HEAD > /tmp/commit
+# git rev-parse --abbrev-ref HEAD > /tmp/branch
+# cat .gitlab-ci.yml /tmp
+#
+# # move to the 'pages' branch and commit the documentation there
+# git checkout pages
+# mkdir -p docs
+# git rm --ignore-unmatch -r docs > /dev/null
+# cp -r ${DOC_PATH} docs
+# git add docs
+# # we ensure that the CI configuration is present on the 'pages' branch,
+# # otherwise pushing from there may not deploy as expected.
+# cp /tmp/.gitlab-ci.yml .
+# git add .gitlab-ci.yml
+# git commit -m "documentation for $(cat /tmp/branch) ($(cat /tmp/commit))" \
+# && git checkout $(cat /tmp/branch) \
+# || git checkout $(cat /tmp/branch)
+#
+# echo
+# echo "The documentation was committed to the 'pages' branch."
+# echo "You can now push it with"
+# echo " git push origin pages"
+#
+pages:
+ # Hardcoded values in the job:
+ # (for Gitlab to understand that this job builds the Pages)
+ # - the job name must be 'pages'
+ # - the stage must be 'deploy'
+ # - the artifacts must be a 'public' directory
+
+ stage: deploy
+
+ # no need for an OCaml environment
+ image: alpine:latest
+
+ # no cache
+
+ # run this job only in the 'pages' branch
+ rules:
+ # https://docs.gitlab.com/ee/ci/yaml/#rules
+ - if: '$CI_COMMIT_REF_NAME == "pages"'
+ when: on_success
+ artifacts:
+ paths:
+ - public
+ script:
+ - rm -fR public/
+ - mkdir -p docs
+ - cp -r docs public
+
+
+
+## MIT License
+#
+# Copyright 2021 Gabriel Scherer
+#
+# Permission is hereby granted, free of charge, to any person obtaining
+# a copy of this software and associated documentation files
+# (the "Software"), to deal in the Software without restriction,
+# including without limitation the rights to use, copy, modify, merge,
+# publish, distribute, sublicense, and/or sell copies of the Software,
+# and to permit persons to whom the Software is furnished to do so,
+# subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be
+# included in all copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+# LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+# OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+# WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/.merlin b/.merlin
deleted file mode 100644
index 1a23de0d..00000000
--- a/.merlin
+++ /dev/null
@@ -1,43 +0,0 @@
-S src
-S src/backends
-S src/backends/C
-S src/backends/EMF
-S src/backends/Horn
-S src/backends/Java
-S src/checks
-S src/features
-S src/features/machine_types
-S src/parsers
-S src/plugins
-S src/plugins/mpfr
-S src/plugins/salsa
-S src/plugins/scopes
-S src/tools
-S src/tools/stateflow
-S src/tools/stateflow/common
-S src/tools/stateflow/json-parser
-S src/tools/stateflow/models
-S src/tools/stateflow/semantics
-S src/utils
-
-B src/_build
-B src/_build/backends
-B src/_build/backends/C
-B src/_build/backends/EMF
-B src/_build/backends/Horn
-B src/_build/checks
-B src/_build/features
-B src/_build/features/machine_types
-B src/_build/parsers
-B src/_build/plugins
-B src/_build/plugins/mpfr
-B src/_build/plugins/salsa
-B src/_build/plugins/scopes
-B src/_build/tools
-B src/_build/tools/stateflow
-B src/_build/tools/stateflow/common
-B src/_build/tools/stateflow/models
-B src/_build/tools/stateflow/semantics
-B src/_build/utils
-
-B test
diff --git a/README.md b/README.md
index f6ee55c5..9c81bfb2 100644
--- a/README.md
+++ b/README.md
@@ -10,14 +10,22 @@ LustreC is a modular compiler of Lustre code into C and Horn Clauses.
# Dependencies
On a fresh ubuntu/debian-like install
-> apt-get install opam libmpfr-dev
+ ```
+ apt-get install opam libmpfr-dev
+ ```
Get a fresh version of ocaml
-> opam switch 4.06.1
+ ```
+opam switch create 4.06.1
+ ```
Install some dependencies
-> opam install depext ocamlgraph mlmpfr num cmdliner fmt logs yojson menhir
+ ```
+opam install depext ocamlgraph mlmpfr num cmdliner fmt logs yojson menhir
+ ```
In OSX, some issues with Z3, please pin the following version:
-> opam pin add z3 4.8.1
-> opam install z3
+ ```
+opam pin add z3 4.8.1
+opam install z3
+ ```
# Build
```
> autoconf
diff --git a/dune-project b/dune-project
new file mode 100644
index 00000000..8bd22308
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,32 @@
+(lang dune 2.8)
+(name lustrec)
+(version 1.7)
+
+(using dune_site 0.1)
+(using menhir 2.0)
+(generate_opam_files true)
+
+(license LGPL)
+(authors "Pierre-Loic Garoche <ploc@garoche.net>"
+ "Xavier Thirioux <thirioux@enseeiht.fr>")
+(maintainers "Pierre-Loic Garoche <ploc@garoche.net>")
+(source (uri git+https://cavale.enseeiht.fr/git/lustrec#unstable))
+(bug_reports https://cavale.enseeiht.fr/redmine/projects/lustrec/issues)
+(homepage https://cavale.enseeiht.fr/redmine/projects/lustrec/)
+
+(package
+ (name lustrec)
+ (sites
+ (lib plugins)
+ (lib verifiers))
+ (synopsis "A Lustre compiler toolset")
+ (description
+ "lustrec is structured around the modular compilation scheme proposed by \
+ Biernacki, Colaço, Hamon, and Pouzet at LCTES'08. It is an open source \
+ lustre compiler that provides verification capabilities. It is currently \
+ mainly used through the CocoSim platform, a Matlab toolbox to perform V&V \
+ of Simulink models. Within CocoSim, the Lustre language is used as an \
+ intermediate representation and relies mainly on lustrec to produce code \
+ or verification artifacts.")
+ (depends ocamlgraph menhir conf-mpfr)
+ (depopts z3 yojson))
diff --git a/lustrec.opam b/lustrec.opam
new file mode 100644
index 00000000..5b331bac
--- /dev/null
+++ b/lustrec.opam
@@ -0,0 +1,33 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "1.7"
+synopsis: "A Lustre compiler toolset"
+description:
+ "lustrec is structured around the modular compilation scheme proposed by Biernacki, Colaço, Hamon, and Pouzet at LCTES'08. It is an open source lustre compiler that provides verification capabilities. It is currently mainly used through the CocoSim platform, a Matlab toolbox to perform V&V of Simulink models. Within CocoSim, the Lustre language is used as an intermediate representation and relies mainly on lustrec to produce code or verification artifacts."
+maintainer: ["Pierre-Loic Garoche <ploc@garoche.net>"]
+authors: [
+ "Pierre-Loic Garoche <ploc@garoche.net>"
+ "Xavier Thirioux <thirioux@enseeiht.fr>"
+]
+license: "LGPL"
+homepage: "https://cavale.enseeiht.fr/redmine/projects/lustrec/"
+bug-reports: "https://cavale.enseeiht.fr/redmine/projects/lustrec/issues"
+depends: [
+ "dune" {>= "2.8"}
+ "odoc" {with-doc}
+]
+build: [
+ ["dune" "subst"] {dev}
+ [
+ "dune"
+ "build"
+ "-p"
+ name
+ "-j"
+ jobs
+ "@install"
+ "@runtest" {with-test}
+ "@doc" {with-doc}
+ ]
+]
+dev-repo: "git+https://cavale.enseeiht.fr/git/lustrec#unstable"
diff --git a/opam b/opam
deleted file mode 100644
index 093cbb76..00000000
--- a/opam
+++ /dev/null
@@ -1,44 +0,0 @@
-opam-version: "2.0"
-name: "lustrec"
-version: "1.7"
-maintainer: "Pierre-Loic Garoche <ploc@garoche.net>"
-authors: ["Pierre-Loic Garoche <ploc@garoche.net>" "Xavier Thirioux <thirioux@enseeiht.fr>"]
-homepage: "https://cavale.enseeiht.fr/redmine/projects/lustrec/"
-bug-reports: "https://cavale.enseeiht.fr/redmine/projects/lustrec/issues"
-license: "LGPL"
-dev-repo: "git+https://cavale.enseeiht.fr/git/lustrec#unstable"
-build: [
- ["autoconf"]
- ["./configure" "--prefix=%{prefix}%"]
- [make]
-]
-install: [make "install"]
-remove: [make "uninstall"]
-depends: [
- "ocamlfind"
- "yojson"
- "cmdliner"
- "fmt"
- "ppx_deriving_yojson"
- "ppx_traverse_builtins"
- "ppxlib"
- "menhir"
- "ocamlgraph"
- "logs"
- "z3"
- "num"
-]
-synopsis: "A Lustre compiler toolset"
-description: """
-lustrec is structured around the modular compilation scheme proposed
-by Biernacki, Colaço, Hamon, and Pouzet at LCTES'08. It is an open
-source lustre compiler that provides verification capabilities.
-It is currently mainly used through the CocoSim platform, a Matlab
-toolbox to perform V&V of Simulink models. Within CocoSim, the Lustre
-language is used as an intermediate representation and relies mainly
-on lustrec to produce code or verification artifacts.
-"""
-url {
- src: "https://cavale.enseeiht.fr/redmine/attachments/download/117/lustrec-1.6-Xia-Zhu-src.tgz"
- checksum: "md5=f06e87d5fbb24c91894bdc55bf6cc496"
-}
diff --git a/src/.merlin b/src/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/arrow.ml b/src/arrow.ml
index 1ce3b268..610b4792 100644
--- a/src/arrow.ml
+++ b/src/arrow.ml
@@ -23,7 +23,7 @@ let arrow_desc =
node_iscontract = false;
}
-let arrow_top_decl =
+let arrow_top_decl () =
{
top_decl_desc = Node arrow_desc;
top_decl_owner = (Options_management.core_dependency "arrow");
diff --git a/src/arrow.mli b/src/arrow.mli
index ae329a1b..ace9a285 100644
--- a/src/arrow.mli
+++ b/src/arrow.mli
@@ -1,3 +1,3 @@
val arrow_id: string
-val arrow_top_decl: Lustre_types.top_decl
+val arrow_top_decl: unit -> Lustre_types.top_decl
val arrow_desc: Lustre_types.node_desc
diff --git a/src/backends/.merlin b/src/backends/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/backends/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/Ada/.merlin b/src/backends/Ada/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/backends/Ada/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/C/.merlin b/src/backends/C/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/backends/C/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index fb1d06a1..cff0245a 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -45,9 +45,9 @@ let print_import_standard fmt =
fprintf fmt "#include <mpfr.h>@."
end;
if !Options.cpp then
- fprintf fmt "#include \"%s/arrow.hpp\"@.@." Arrow.arrow_top_decl.top_decl_owner
+ fprintf fmt "#include \"%s/arrow.hpp\"@.@." (Arrow.arrow_top_decl ()).top_decl_owner
else
- fprintf fmt "#include \"%s/arrow.h\"@.@." Arrow.arrow_top_decl.top_decl_owner
+ fprintf fmt "#include \"%s/arrow.h\"@.@." (Arrow.arrow_top_decl ()).top_decl_owner
end
diff --git a/src/backends/EMF/.merlin b/src/backends/EMF/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/backends/EMF/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/Horn/.merlin b/src/backends/Horn/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/backends/Horn/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/Java/.merlin b/src/backends/Java/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/backends/Java/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/checks/.merlin b/src/checks/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/checks/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/checks/liveness.ml b/src/checks/liveness.ml
index dd6c48aa..542344b3 100644
--- a/src/checks/liveness.ml
+++ b/src/checks/liveness.ml
@@ -12,7 +12,6 @@
open Utils
open Lustre_types
open Corelang
-open Graph
open Causality
type context =
diff --git a/src/dune b/src/dune
new file mode 100644
index 00000000..8690c7da
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,128 @@
+(env
+ (dev
+ (flags (:standard -warn-error -A))))
+
+(include_subdirs unqualified)
+
+(library
+ (name lustrec_interface)
+ (package lustrec)
+ (modules
+ lustre_types
+ utils
+ lustre_utils
+ location
+ dimension
+ env
+ real
+ types
+ options
+ version
+ clocks
+ delay
+ machine_code_types
+ scheduling_type
+ log
+ printers
+ corelang
+ basic_library
+ type_predef
+ clock_predef
+ delay_predef
+ error
+ global
+ annotations
+ machine_code_common
+ arrow
+ options_management
+ stateless
+ c_backend_common
+ typing
+ ocaml_utils
+ backends
+ lustrec_mpfr
+ normalization
+ machine_types
+ splitting
+ compiler_common
+ parse parser_lustre lexer_lustre lexerLustreSpec
+ automata
+ clock_calculus
+ )
+ (wrapped false)
+ (libraries ocamlgraph zarith unix str))
+
+(library
+ (name plugin_register)
+ (package lustrec)
+ (wrapped false)
+ (modules pluginList pluginType)
+ (libraries lustrec_interface))
+
+(generate_sites_module
+ (module sites)
+ (plugins (lustrec plugins) (lustrec verifiers)))
+
+(library
+ (name sites)
+ (package lustrec)
+ (modules sites)
+ (libraries dune-site dune-site.plugins))
+
+(library
+ (name lustrec_lib)
+ (package lustrec)
+ (modules
+ lusic
+ c_backend_header c_backend_spec c_backend_makefile
+ c_backend_lusic c_backend_mauve c_backend_src
+ ada_backend ada_printer ada_backend_common ada_backend_ads ada_backend_adb
+ ada_backend_wrapper
+ horn_backend horn_backend_common horn_backend_printers
+ Horn_backend_collecting_sem horn_backend_traces
+ EMF_backend EMF_common EMF_library_calls
+ misc_lustre_function misc_printer
+ machine_code
+ causality
+ scheduling
+ liveness
+ compiler_stages
+ modules
+ sortProg
+ inliner
+ access
+ algebraicLoop
+ optimize_prog
+ optimize_machine
+ spec
+ c_backend c_backend_main
+ plugins
+ )
+ (wrapped false)
+ (libraries sites lustrec_interface plugin_register))
+
+(executable
+ (name main_lustre_compiler)
+ (public_name lustrec)
+ (modules main_lustre_compiler)
+ (package lustrec)
+ (libraries lustrec_lib lustrec.scopes))
+
+(executable
+ (name main_lustre_testgen)
+ (public_name lustret)
+ (modules main_lustre_testgen mutation mmap pathConditions)
+ (libraries lustrec_lib))
+
+(library
+ (name verifier_register)
+ (package lustrec)
+ (wrapped false)
+ (modules verifierList verifierType)
+ (libraries lustrec_interface))
+
+(executable
+ (name main_lustre_verifier)
+ (public_name lustrev)
+ (modules main_lustre_verifier verifiers)
+ (libraries lustrec_lib verifier_register lustrec.scopes))
diff --git a/src/features/.merlin b/src/features/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/features/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/features/machine_types/.merlin b/src/features/machine_types/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/features/machine_types/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/machine_code.ml b/src/machine_code.ml
index c964e96d..e80233bf 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -227,12 +227,12 @@ let translate_eq env ctx eq =
match eq.eq_lhs, eq.eq_rhs.expr_desc with
| [x], Expr_arrow (e1, e2) ->
let var_x = env.get_var x in
- let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
+ let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
let c1 = translate_expr e1 in
let c2 = translate_expr e2 in
{ ctx with
si = mkinstr (MReset o) :: ctx.si;
- j = Utils.IMap.add o (Arrow.arrow_top_decl, []) ctx.j;
+ j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
s = (control_on_clock
eq.eq_rhs.expr_clock
(mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))
diff --git a/src/ocaml_utils.ml.in b/src/ocaml_utils.ml.in
deleted file mode 100644
index 09a45753..00000000
--- a/src/ocaml_utils.ml.in
+++ /dev/null
@@ -1 +0,0 @@
-let uppercase = @UPPERCASEFUN@
diff --git a/src/options_management.ml b/src/options_management.ml
index acc58285..cfc14857 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -52,7 +52,8 @@ let search_lib_path (local, full_file_name) =
in
match name with
| None ->
- Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name (Utils.fprintf_list ~sep:", " Format.pp_print_string) paths;
+ Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name
+ (Utils.fprintf_list ~sep:", " Format.pp_print_string) paths;
raise Not_found
| Some s -> s
diff --git a/src/parsers/.merlin b/src/parsers/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/parsers/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/parsers/dune b/src/parsers/dune
new file mode 100644
index 00000000..16d76189
--- /dev/null
+++ b/src/parsers/dune
@@ -0,0 +1,12 @@
+; (include_subdirs no)
+
+; (library
+; (name parse)
+; (package lustrec)
+; (wrapped false)
+; (libraries lustre_types corelang automata))
+
+(menhir
+ (modules parser_lustre))
+
+(ocamllex lexerLustreSpec lexer_lustre)
diff --git a/src/parsers/parse.ml b/src/parsers/parse.ml
index 69909045..c33319cf 100644
--- a/src/parsers/parse.ml
+++ b/src/parsers/parse.ml
@@ -9,8 +9,6 @@
(* *)
(********************************************************************)
open Format
-open Lustre_types
-open Corelang
type error =
| Undefined_token of string
diff --git a/src/pluginList.ml.in b/src/pluginList.ml.in
deleted file mode 100644
index 6efbd219..00000000
--- a/src/pluginList.ml.in
+++ /dev/null
@@ -1,5 +0,0 @@
-let plugins =
- [
- (module Scopes.Plugin : PluginType.S);
- @SALSA@
- ]
diff --git a/src/plugins/.merlin b/src/plugins/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/plugins/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/plugins/mpfr/.merlin b/src/plugins/mpfr/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/plugins/mpfr/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/plugins/pluginList.ml b/src/plugins/pluginList.ml
new file mode 100644
index 00000000..ad10f547
--- /dev/null
+++ b/src/plugins/pluginList.ml
@@ -0,0 +1,3 @@
+let registered : (module PluginType.S) list ref = ref []
+
+let plugins () = !registered
diff --git a/src/pluginType.ml b/src/plugins/pluginType.ml
similarity index 100%
rename from src/pluginType.ml
rename to src/plugins/pluginType.ml
diff --git a/src/plugins.ml b/src/plugins/plugins.ml
similarity index 85%
rename from src/plugins.ml
rename to src/plugins/plugins.ml
index 219d4e56..e7e9689d 100644
--- a/src/plugins.ml
+++ b/src/plugins/plugins.ml
@@ -2,6 +2,7 @@ open Lustre_types
open PluginList
+let () = Sites.Plugins.Plugins.load_all ()
let options () =
List.flatten (
@@ -9,37 +10,37 @@ let options () =
List.map (fun m ->
let module M = (val m : PluginType.S) in
(M.name, M.activate, M.usage, M.options)
- ) plugins
+ ) (plugins ())
))
let init () =
List.iter (fun m ->
let module M = (val m : PluginType.S) in
M.init ()
- ) plugins
+ ) (plugins ())
let check_force_stateful () =
List.exists (fun m ->
let module M = (val m : PluginType.S) in
M.check_force_stateful ()
- ) plugins
+ ) (plugins ())
let refine_machine_code prog machine_code =
List.fold_left (fun accu m ->
let module M = (val m : PluginType.S) in
M.refine_machine_code prog accu
- ) machine_code plugins
+ ) machine_code (plugins ())
let c_backend_main_loop_body_prefix basename mname fmt () =
List.iter (fun (m: (module PluginType.S)) ->
let module M = (val m : PluginType.S) in
- M.c_backend_main_loop_body_prefix basename mname fmt ()) plugins
+ M.c_backend_main_loop_body_prefix basename mname fmt ()) (plugins ())
let c_backend_main_loop_body_suffix fmt () =
List.iter (fun (m: (module PluginType.S)) ->
let module M = (val m : PluginType.S) in
- M.c_backend_main_loop_body_suffix fmt ()) plugins
+ M.c_backend_main_loop_body_suffix fmt ()) (plugins ())
(* Specific treatment of annotations when inlining, specific of declared plugins *)
diff --git a/src/plugins/salsa/.merlin b/src/plugins/salsa/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/plugins/salsa/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/plugins/salsa/dune b/src/plugins/salsa/dune
new file mode 100644
index 00000000..70fbbfff
--- /dev/null
+++ b/src/plugins/salsa/dune
@@ -0,0 +1,13 @@
+(include_subdirs no)
+
+(library
+ (name salsa_plugin)
+ (public_name lustrec.salsa_plugin)
+ (libraries lustrec_interface plugin_register salsa)
+ (optional))
+
+(plugin
+ (name salsa_plugin)
+ (libraries lustrec.salsa_plugin)
+ (site (lustrec plugins))
+ (optional))
diff --git a/src/plugins/salsa/salsa_plugin.ml b/src/plugins/salsa/salsa_plugin.ml
index 1bbf6ca2..a16909ab 100644
--- a/src/plugins/salsa/salsa_plugin.ml
+++ b/src/plugins/salsa/salsa_plugin.ml
@@ -54,3 +54,7 @@ module Plugin =
end: PluginType.S)
+
+let () =
+ PluginList.registered := (module Plugin : PluginType.S) ::
+ !PluginList.registered
diff --git a/src/plugins/scopes/.merlin b/src/plugins/scopes/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/plugins/scopes/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/plugins/scopes/dune b/src/plugins/scopes/dune
new file mode 100644
index 00000000..b110b1f3
--- /dev/null
+++ b/src/plugins/scopes/dune
@@ -0,0 +1,11 @@
+(include_subdirs no)
+
+(library
+ (name scopes)
+ (public_name lustrec.scopes)
+ (libraries lustrec_interface plugin_register))
+
+(plugin
+ (name scopes_plugin)
+ (libraries lustrec.scopes)
+ (site (lustrec plugins)))
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index ae7e473d..daa75f4c 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -422,7 +422,10 @@ module Plugin : (
end
-
+
+let () =
+ PluginList.registered := (module Plugin : PluginType.S) ::
+ !PluginList.registered
(* Local Variables: *)
(* compile-command:"make -C ../.." *)
(* End: *)
diff --git a/src/tools/.merlin b/src/tools/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/tools/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/seal/dune b/src/tools/seal/dune
new file mode 100644
index 00000000..2f77ac7d
--- /dev/null
+++ b/src/tools/seal/dune
@@ -0,0 +1,13 @@
+(include_subdirs no)
+
+(library
+ (name seal_verifier)
+ (public_name lustrec.seal_verifier)
+ (libraries verifier_register lustrec_lib zustre_verifier)
+ (optional))
+
+(plugin
+ (name seal_verifier)
+ (libraries lustrec.seal_verifier)
+ (site (lustrec verifiers))
+ (optional))
diff --git a/src/tools/seal/seal_verifier.ml b/src/tools/seal/seal_verifier.ml
index 4802d217..fed38147 100644
--- a/src/tools/seal/seal_verifier.ml
+++ b/src/tools/seal/seal_verifier.ml
@@ -157,3 +157,6 @@ module Verifier =
end: VerifierType.S)
+let () =
+ VerifierList.registered := (module Verifier : VerifierType.S) ::
+ !VerifierList.registered
diff --git a/src/tools/stateflow/.merlin b/src/tools/stateflow/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/tools/stateflow/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/common/.merlin b/src/tools/stateflow/common/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/tools/stateflow/common/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/json-parser/.merlin b/src/tools/stateflow/json-parser/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/tools/stateflow/json-parser/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/models/.merlin b/src/tools/stateflow/models/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/tools/stateflow/models/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/semantics/.merlin b/src/tools/stateflow/semantics/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/tools/stateflow/semantics/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/semantics/cPS_evaluator.ml b/src/tools/stateflow/semantics/cPS_evaluator.ml
index 896252ca..c15d501d 100644
--- a/src/tools/stateflow/semantics/cPS_evaluator.ml
+++ b/src/tools/stateflow/semantics/cPS_evaluator.ml
@@ -7,7 +7,7 @@
- Evaluator module
*)
- let _main_ _ =
+ let _main_ _ = function
| Eval ->
let module Model = (val model) in
let module T = CPS_transformer.Evaluator in
diff --git a/src/tools/tiny/dune b/src/tools/tiny/dune
new file mode 100644
index 00000000..2242ea1a
--- /dev/null
+++ b/src/tools/tiny/dune
@@ -0,0 +1,13 @@
+(include_subdirs no)
+
+(library
+ (name tiny_verifier)
+ (public_name lustrec.tiny_verifier)
+ (libraries verifier_register tiny)
+ (optional))
+
+(plugin
+ (name tiny_verifier)
+ (libraries lustrec.tiny_verifier)
+ (site (lustrec verifiers))
+ (optional))
diff --git a/src/tools/tiny/tiny_verifier.ml b/src/tools/tiny/tiny_verifier.ml
index 0f903a21..071e1430 100644
--- a/src/tools/tiny/tiny_verifier.ml
+++ b/src/tools/tiny/tiny_verifier.ml
@@ -135,4 +135,7 @@ module Verifier =
end: VerifierType.S)
-
+
+let () =
+ VerifierList.registered := (module Verifier : VerifierType.S) ::
+ !VerifierList.registered
diff --git a/src/tools/zustre/dune b/src/tools/zustre/dune
new file mode 100644
index 00000000..0b5140f9
--- /dev/null
+++ b/src/tools/zustre/dune
@@ -0,0 +1,15 @@
+(include_subdirs no)
+
+(library
+ (name zustre_verifier)
+ (public_name lustrec.zustre_verifier)
+ (wrapped false)
+ (modules :standard \ zustre_test)
+ (libraries verifier_register lustrec_lib z3 yojson)
+ (optional))
+
+(plugin
+ (name zustre_verifier)
+ (libraries lustrec.zustre_verifier)
+ (site (lustrec verifiers))
+ (optional))
diff --git a/src/tools/zustre/zustre_verifier.ml b/src/tools/zustre/zustre_verifier.ml
index 12281ff4..337654c9 100644
--- a/src/tools/zustre/zustre_verifier.ml
+++ b/src/tools/zustre/zustre_verifier.ml
@@ -264,7 +264,12 @@ module Verifier =
end: VerifierType.S)
-
+
+
+let () =
+ VerifierList.registered := (module Verifier : VerifierType.S) ::
+ !VerifierList.registered
+
(* Local Variables: *)
(* compile-command:"make -C ../.. lustrev" *)
(* End: *)
diff --git a/src/utils/.merlin b/src/utils/.merlin
deleted file mode 100644
index 2fb3f0bc..00000000
--- a/src/utils/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/dimension.ml b/src/utils/dimension.ml
similarity index 100%
rename from src/dimension.ml
rename to src/utils/dimension.ml
diff --git a/src/utils/dune b/src/utils/dune
new file mode 100644
index 00000000..064da44e
--- /dev/null
+++ b/src/utils/dune
@@ -0,0 +1,18 @@
+; (include_subdirs no)
+
+(rule
+ (target ocaml_utils.ml)
+ (deps ocaml_utils.ml.lt403)
+ (action (copy %{deps} %{target}))
+ (enabled_if (< %{ocaml_version} 4.0.3)))
+(rule
+ (target ocaml_utils.ml)
+ (deps ocaml_utils.ml.ge403)
+ (action (copy %{deps} %{target}))
+ (enabled_if (>= %{ocaml_version} 4.0.3)))
+
+; (library
+; (name utils)
+; (package lustrec)
+; (wrapped false)
+; (libraries ocamlgraph unix))
diff --git a/src/location.ml b/src/utils/location.ml
similarity index 100%
rename from src/location.ml
rename to src/utils/location.ml
diff --git a/src/utils/ocaml_utils.ml.ge403 b/src/utils/ocaml_utils.ml.ge403
new file mode 100644
index 00000000..90fadc64
--- /dev/null
+++ b/src/utils/ocaml_utils.ml.ge403
@@ -0,0 +1 @@
+let uppercase = String.uppercase_ascii
diff --git a/src/utils/ocaml_utils.ml.lt403 b/src/utils/ocaml_utils.ml.lt403
new file mode 100644
index 00000000..41db848f
--- /dev/null
+++ b/src/utils/ocaml_utils.ml.lt403
@@ -0,0 +1 @@
+let uppercase = String.uppercase
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index 89d1be33..f1c661dc 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -428,7 +428,6 @@ let get_date () =
Format.flush_str_formatter ()
-
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/verifierList.ml b/src/verifierList.ml
new file mode 100644
index 00000000..254cda86
--- /dev/null
+++ b/src/verifierList.ml
@@ -0,0 +1,8 @@
+let registered : (module VerifierType.S) list ref = ref []
+
+let verifiers () = !registered
+ (* [
+ * @LUSTREV_SEAL@
+ * @LUSTREV_ZUSTRE@
+ * @LUSTREV_TINY@
+ * ] *)
diff --git a/src/verifierList.ml.in b/src/verifierList.ml.in
deleted file mode 100644
index 322949a2..00000000
--- a/src/verifierList.ml.in
+++ /dev/null
@@ -1,6 +0,0 @@
-let verifiers =
- [
- @LUSTREV_SEAL@
- @LUSTREV_ZUSTRE@
- @LUSTREV_TINY@
- ]
diff --git a/src/verifiers.ml b/src/verifiers.ml
index e36bfd9e..baac4bc0 100644
--- a/src/verifiers.ml
+++ b/src/verifiers.ml
@@ -2,6 +2,8 @@ open Lustre_types
open VerifierList
+let () = Sites.Plugins.Verifiers.load_all ()
+
let active = ref None
let options () =
@@ -10,7 +12,7 @@ let options () =
List.map (fun m ->
let module M = (val m : VerifierType.S) in
(M.name, M.activate, M.options)
- ) verifiers
+ ) (verifiers ())
))
let verifier_list verifiers =
@@ -31,10 +33,10 @@ let get_active () =
m::found
else
found
- ) [] verifiers
+ ) [] (verifiers ())
in
match found with
- | [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list verifiers))
+ | [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list (verifiers ())))
| [m] -> active := Some m; m
| _ -> raise (Sys_error ("Too many selected verifiers: " ^ verifier_list found))
end
diff --git a/src/version.ml.in b/src/version.ml
similarity index 99%
rename from src/version.ml.in
rename to src/version.ml
index 19e9233c..30f5044e 100644
--- a/src/version.ml.in
+++ b/src/version.ml
@@ -1,4 +1,3 @@
-
let number = "@PACKAGE_VERSION@-@GITBRANCH@"
let codename ="@VERSION_CODENAME@"
--
GitLab