diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5073f7a4d413e63e6b5017146119c00c817970e2..d3600979543f5c057672f0be089f4ccc43a5eeb2 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -71,7 +71,7 @@ check-release:
[[ "$DEFAULT" == "$CI_COMMIT_BRANCH" ]] &&
[[ "$DEFAULT" == "stable/$(cat VERSION_CODENAME | tr '[:upper:]' '[:lower:]')" ]] &&
[[ "$(git describe --tag)" == "$(cat VERSION | sed 's/~/-/')" ]]
- [[ "$(cat VERSION)" == "$(cat opam/opam | grep "^version" | sed 's/version: \"\(.*\)\"/\1/')" ]]
+ [[ "$(cat VERSION)" == "$(cat opam | grep "^version" | sed 's/version: \"\(.*\)\"/\1/')" ]]
only:
variables:
- $RELEASE == "yes"
diff --git a/INSTALL.md b/INSTALL.md
index 4da90aabb490249618619ddef4357f9b3287e0e4..281258aac8f3cf08ad6b696376928a33ca5c7efc 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -312,7 +312,7 @@ Arch Linux: `pikaur -S frama-c`
opam install --deps-only frama-c
If not using [opam](http://opam.ocaml.org/), you will need to install
- the Frama-C dependencies by yourself. The `opam/opam` file in the Frama-C
+ the Frama-C dependencies by yourself. The `opam` file in the Frama-C
.tar.gz lists the required dependencies (e.g. `ocamlfind`, `ocamlgraph`,
`zarith`, etc.). A few of these dependencies are optional, only required
for the graphical interface: `lablgtk`, `conf-gnomecanvas` and
@@ -334,7 +334,7 @@ Arch Linux: `pikaur -S frama-c`
#### Frama-C Requirements
-See the `opam/opam` file, section `depends`, for compatible OCaml versions and
+See the `opam` file, section `depends`, for compatible OCaml versions and
required dependencies (except for those related to `lablgtk`, which are
required for the GUI but otherwise optional).
diff --git a/Makefile b/Makefile
index db4b105ede7d37525f0b873ea747a5b5ba28703b..458c48a190606e107506fba09460c33697b62c19 100644
--- a/Makefile
+++ b/Makefile
@@ -74,6 +74,7 @@ help::
################################
include share/Makefile.installation
+include ivette/Makefile.installation
###############################################################################
# HEADER MANAGEMENT
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index fbc41f1c1abada51e201b289c1bcfd270f89f036..5483cd53a5ad30c8cd83a9de349d5a5089ab98b7 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -816,7 +816,7 @@ case "${STEP}" in
9)
step 9 "GENERATE OPAM FILE"
assert_out_dir
- cat opam/opam | grep -v "^version\:" | grep -v "^name\:" > $OUT_DIR/opam
+ cat opam | grep -v "^version\:" | grep -v "^name\:" > $OUT_DIR/opam
echo >> "$OUT_DIR/opam"
echo "url {" >> "$OUT_DIR/opam"
echo " src: \"https://git.frama-c.com/pub/frama-c/-/wikis/downloads/$TARGZ_FILENAME\"" >> "$OUT_DIR/opam"
diff --git a/dev/build-release.sh b/dev/build-release.sh
index 3e43b4135ad4fc7360240489574d2597a67d68a5..288dd2269e7da7ed0b747b5f74ff107c476576d2 100755
--- a/dev/build-release.sh
+++ b/dev/build-release.sh
@@ -264,7 +264,7 @@ OPAM_FC_DIR="$OPAM_DIR/packages/frama-c/frama-c.$VERSION"
mkdir -p $OPAM_DIR
mkdir -p $OPAM_FC_DIR
-cat opam/opam | grep -v "^version\:" | grep -v "^name\:" > $OPAM_FC_DIR/opam
+cat opam | grep -v "^version\:" | grep -v "^name\:" > $OPAM_FC_DIR/opam
cat >>$OPAM_FC_DIR/opam << EOL
url {
diff --git a/dev/make-distrib.sh b/dev/make-distrib.sh
index 2000ad90ec86bf4c0753ee2ea0d6295e41da03d0..b57c2da9cb48d6161d1de2def1025b891f29b5d7 100755
--- a/dev/make-distrib.sh
+++ b/dev/make-distrib.sh
@@ -53,7 +53,7 @@ FRAMAC_TAR="$FRAMAC.tar"
################################################################################
# Check Opam file
-OPAM_VERSION=$(cat opam/opam | grep "^version" | sed 's/version: \"\(.*\)\"/\1/')
+OPAM_VERSION=$(cat opam | grep "^version" | sed 's/version: \"\(.*\)\"/\1/')
if [ "$VERSION" != "$OPAM_VERSION" ]; then
echo "VERSION ($VERSION) and OPAM_VERSION ($OPAM_VERSION) differ"
diff --git a/doc/release/validation.tex b/doc/release/validation.tex
index 5a73843cb085290b46dfe7605d806ce4e11580e7..89b21b4ba58e9e1991ae64afce01283dca5c8709 100644
--- a/doc/release/validation.tex
+++ b/doc/release/validation.tex
@@ -9,7 +9,7 @@ Install all dependencies of Frama-C, including recommended ones.
Check coherence between:
\begin{itemize}
- \item \texttt{opam/opam} \todo{Should always be up to date}
+ \item \texttt{opam} \todo{Should always be up to date}
\item \texttt{reference-configuration.md} \todo{Should always be up to date}
\end{itemize}
@@ -42,7 +42,7 @@ Check the following files:
\item \texttt{src/plugins/wp/Changelog}
\item \texttt{src/plugins/e-acsl/doc/Changelog}
\item \texttt{INSTALL.md} ("Reference configuration")
- \item \texttt{opam/opam} (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
+ \item \texttt{opam} (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
\end{itemize}
\subsection{Versions in source: API documentation}
@@ -101,7 +101,7 @@ Manuals experts:
\subsection{Contributors}
Update the Frama-C's authors list in files
-\texttt{src/plugins/gui/help\_manager.ml} and \texttt{opam/opam}. Traditionally,
+\texttt{src/plugins/gui/help\_manager.ml} and \texttt{opam}. Traditionally,
an author is added if they have contributed 100+ LoC in the release, as counted
by:
\begin{verbatim}
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index 0810f44626e3c42cd861c0b98f0c68eaa91c6cd3..ebabe0499ebaf6230e38ae0642cac3168264c959 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -23,7 +23,7 @@ binary package for the considered platform.
Finally, \FramaC can be compiled and installed from the source distribution,
as long as its dependencies have already been installed. The exact set of
dependencies varies from release to release. They are listed as constraints
-in the \texttt{opam/opam} file of the source distribution.
+in the \texttt{opam} file of the source distribution.
A {\em reference configuration}, guaranteed to be a working set of dependencies
for \FramaC kernel and the open-source plug-ins included in the source
@@ -47,11 +47,11 @@ and running \FramaC are described below.
\item[The \caml compiler]\index{OCaml compiler}\footnote{\url{http://ocaml.org}}
is required both for compiling \FramaC from source \emph{and} for compiling
additional plug-ins. Compatible OCaml versions are listed as constraints in
- the \texttt{opam/opam} file.
+ the \texttt{opam} file.
\end{description}
Other components, such as OcamlGraph, Zarith, Gtk-related packages for the GUI,
-etc., are listed in the \texttt{INSTALL.md} and \texttt{opam/opam} files.
+etc., are listed in the \texttt{INSTALL.md} and \texttt{opam} files.
\section{One Framework, Several Executables}\label{sec:modes}
diff --git a/ivette/Makefile b/ivette/Makefile
index cefa700bb4bedc2794841313cbecbace333f60ac..510191e354240fa786f2550c338a4112f574c819 100644
--- a/ivette/Makefile
+++ b/ivette/Makefile
@@ -31,13 +31,16 @@ DOME_CUSTOM_ENTRIES= yes
COPYRIGHT=CEA LIST / LSL
# --------------------------------------------------------------------------
-.PHONY: all app dev pkg doc serve dist lint fixlint checkcase
+# --------------------------------------------------------------------------
+# --- Ivette Compilation
+# --------------------------------------------------------------------------
+
+.PHONY: all app dev lint checkcase tsc
all: pkg lint app
app: dome-app
dev: dome-dev
-dist: dist-dir dome-dist
lint: dome-pkg dome-templ checkcase
@echo "[Ivette] running typechecker & linter"
@@ -68,10 +71,24 @@ help::
@echo "Ivette installation configuration variables"
@echo " - PREFIX: used to customize installation path"
+# --------------------------------------------------------------------------
+# --- Ivette Distribution
+# --------------------------------------------------------------------------
+
+.PHONY: dist dist-dir
+
+dist-dir:
+ @echo "Cleaning dist"
+ @rm -fr dist
+
+dist: dist-dir dome-dist
+
# --------------------------------------------------------------------------
# --- Ivette Package Loader
# --------------------------------------------------------------------------
+.PHONY: pkg
+
LOADER=src/renderer/loader.ts
SANDBOX=src/renderer/sandbox.ts
PACKAGES=$(shell find src -name "pkg.json")
@@ -158,13 +175,11 @@ include $(DOME)/template/makefile
# --- Ivette Installation
# --------------------------------------------------------------------------
+.PHONY: install
+
BINDIR=$(PREFIX)/bin
LIBDIR=$(PREFIX)/lib
-dist-dir:
- @echo "Cleaning dist"
- @rm -fr dist
-
UNAME=$(shell uname)
ifeq ($(UNAME),Darwin)
@@ -189,25 +204,32 @@ endif
IVETTE_DIST=$(wildcard dist/linux-unpacked dist/mac dist/mac-arm64)
-ifdef LIBDIR
-ifdef BINDIR
+ifdef PREFIX
ifeq ($(IVETTE_DIST),dist/linux-unpacked)
install:
@echo "Installing Ivette (Linux)"
- @rm -fr $(LIBDIR)/ivette
+ @mkdir -p $(LIBDIR)/frama-c
+ @rm -fr $(LIBDIR)/frama-c/ivette
+ @mv $(IVETTE_DIST) $(LIBDIR)/frama-c/ivette
+ @mkdir -p $(BINDIR)
@rm -f $(BINDIR)/ivette
- @mv $(IVETTE_DIST) $(LIBDIR)/ivette
- @ln -s $(LIBDIR)/ivette/ivette $(BINDIR)/ivette
+ @ln -s $(LIBDIR)/frama-c/ivette/ivette $(BINDIR)/ivette
else ifeq ($(IVETTE_DIST:-arm64=),dist/mac)
install:
@echo "Installing Ivette (macOS)"
- @rm -fr /Applications/Ivette.app
- @mv $(IVETTE_DIST)/Ivette.app /Applications/
+ @mkdir -p $(LIBDIR)/frama-c
+ @rm -fr $(LIBDIR)/frama-c/Ivette.app
+ @mv $(IVETTE_DIST)/Ivette.app $(LIBDIR)/frama-c/
+ @cp ivette-macos.sh dist/ivette.sh
+ @echo "exec open -na $(LIBDIR)/frama-c/Ivette.app --args\\" >> dist/ivette.sh
+ @echo " --command $(BINDIR)/frama-c\\" >> dist/ivette.sh
+ @echo " --working \$$PWD \$$*" >> dist/ivette.sh
+ @mkdir -p $(BINDIR)
+ @install dist/ivette.sh $(BINDIR)/ivette
@rm -fr $(IVETTE_DIST)
- @install ivette-macos.sh $(BINDIR)/ivette
else
@@ -217,24 +239,27 @@ install:
@exit 1
endif
-endif
+else
+
+install:
+ @echo "PREFIX not defined"
+ @exit 1
+
endif
# --------------------------------------------------------------------------
# --- Ivette Un-Installation
# --------------------------------------------------------------------------
-ifdef LIBDIR
-ifdef BINDIR
+ifdef PREFIX
uninstall:
@echo "Uninstall Ivette"
- @rm -fr dist
- @rm -fr /Applications/Ivette.app
- @rm -fr $(LIBDIR)/ivette
- @rm -f $(BINDIR)/ivette
+ @rm -f $(BINDIR)/ivette
+ @rm -f $(LIBDIR)/frama-c/ivette.tgz
+ @rm -fr $(LIBDIR)/frama-c/Ivette.app
+ @rm -fr $(LIBDIR)/frama-c/ivette
endif
-endif
# --------------------------------------------------------------------------
diff --git a/ivette/Makefile.installation b/ivette/Makefile.installation
new file mode 100644
index 0000000000000000000000000000000000000000..9f302b06dd1e3a566ab63650dd62c2b02ea425d8
--- /dev/null
+++ b/ivette/Makefile.installation
@@ -0,0 +1,55 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# --------------------------------------------------------------------------
+# --- OPAM Installation
+# --------------------------------------------------------------------------
+
+FILTER= \
+ --exclude-vcs \
+ --exclude "doc" \
+ --exclude "dist" \
+ --exclude "tests" \
+ --exclude "_build" \
+ --exclude "node_modules" \
+
+ifndef PREFIX
+then
+install::
+ @echo "Warning: not target for Ivette"
+ @echo " (no PREFIX, nor OPAM_SWITCH_PREFIX)"
+else
+install::
+ @echo "Installing Ivette to ${PREFIX}"
+ @mkdir -p ${PREFIX}/bin
+ @install ivette/ivette-bootstrap.sh ${PREFIX}/bin/ivette
+ @mkdir -p ${PREFIX}/lib/frama-c
+ @tar zcf ${PREFIX}/lib/frama-c/ivette.tgz ${FILTER} ivette
+
+uninstall::
+ @echo "Removing Ivette"
+ @rm -f ${PREFIX}/bin/ivette
+ @rm -f ${PREFIX}/lib/frama-c/ivette.tgz
+ @rm -fr ${PREFIX}/lib/frama-c/Ivette.app
+ @rm -fr ${PREFIX}/lib/frama-c/ivette
+
+endif
diff --git a/ivette/api.sh b/ivette/api.sh
index ad8c7690a9ffee9809ff52f0b12c48a5a685a9c2..4bb7807873bc13dc944e883d388f3c0400cfe720 100755
--- a/ivette/api.sh
+++ b/ivette/api.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#! /usr/bin/env bash
##########################################################################
# #
# This file is part of Frama-C. #
diff --git a/ivette/ivette-bootstrap.sh b/ivette/ivette-bootstrap.sh
new file mode 100755
index 0000000000000000000000000000000000000000..02522fc000885de99ea7ff434874f22e38197ef8
--- /dev/null
+++ b/ivette/ivette-bootstrap.sh
@@ -0,0 +1,122 @@
+#! /usr/bin/env bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# --------------------------------------------------------------------------
+# --- Ivette bootstrapper for OPAM installation
+# --------------------------------------------------------------------------
+
+echo "Building Ivette"
+USERCWD=`pwd`
+
+# --------------------------------------------------------------------------
+
+function InstallHelp()
+{
+ echo "Ivette Requirements:"
+ echo " - node v16"
+ echo " - yarn (any version)"
+ echo "Recommanded Installation:"
+ echo " - install nvm (https://github.com/nvm-sh/nvm)"
+ echo " - run 'nvm use 16'"
+ echo " - run 'npm install --global yarn'"
+ echo " - run 'ivette'"
+}
+
+# --------------------------------------------------------------------------
+echo "[1/3] Configuring"
+# --------------------------------------------------------------------------
+
+NODEJS=`node --version`
+case $NODEJS in
+ v16.*)
+ echo " - node $NODEJS found"
+ ;;
+ *)
+ echo "Ivette requires node version 16 to be installed."
+ echo
+ InstallHelp
+ exit 1 ;;
+esac
+
+YARNJS=`yarn --version`
+case $YARNJS in
+ 1.*)
+ echo " - yarn $YARNJS found"
+ ;;
+ *)
+ echo "Ivette requires yarn to be installed."
+ echo
+ InstallHelp
+ exit 1
+ ;;
+esac
+
+SELF=`dirname $0`
+cd $SELF/..
+PREFIX=`pwd`
+
+if [ -f $PREFIX/lib/frama-c/ivette.tgz ]
+then
+ echo " - prefix $PREFIX"
+else
+ echo "Ivette archive not found ($PREFIX)"
+ exit 1
+fi
+
+# --------------------------------------------------------------------------
+echo "[2/3] Compiling Ivette"
+# --------------------------------------------------------------------------
+
+TMPDIR=`mktemp -d`
+cd $TMPDIR
+tar zxf $PREFIX/lib/frama-c/ivette.tgz
+cd ivette
+make dist
+if [ "$?" != "0" ]
+then
+ echo "Compilation Failed"
+ rm -fr $TMPDIR
+ exit 2
+fi
+
+# --------------------------------------------------------------------------
+echo "[3/3] Finalizing Installation"
+# --------------------------------------------------------------------------
+
+make PREFIX=$PREFIX install
+if [ "$?" != "0" ]
+then
+ echo "Installation Failed"
+ rm -fr $TMPDIR
+ exit 3
+fi
+cd $USERCWD
+rm -fr $TMPDIR
+rm -f $PREFIX/lib/frama-c/ivette.tgz
+
+# --------------------------------------------------------------------------
+echo "Launching Ivette..."
+# --------------------------------------------------------------------------
+exec $PREFIX/bin/ivette $*
+
+# --------------------------------------------------------------------------
diff --git a/ivette/ivette-macos.sh b/ivette/ivette-macos.sh
index d96a421f382fbb17dea3f88b637b15f3a199a6c6..d84cd52ee455a840f993ca13443b10fbb6d9919f 100755
--- a/ivette/ivette-macos.sh
+++ b/ivette/ivette-macos.sh
@@ -1,4 +1,4 @@
-#!/bin/zsh
+#! /usr/bin/env bash
##########################################################################
# #
# This file is part of Frama-C. #
@@ -20,5 +20,3 @@
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
-
-exec open -na /Applications/Ivette.app --args --working $PWD $*
diff --git a/ivette/src/dome/template/export.sh b/ivette/src/dome/template/export.sh
index 6cdae2a4802e0931935cf2ef7d504c4844b733ae..bc4db7744176277e35a123a81b751787f3c97927 100755
--- a/ivette/src/dome/template/export.sh
+++ b/ivette/src/dome/template/export.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#! /usr/bin/env bash
##########################################################################
# #
# This file is part of Frama-C. #
diff --git a/ivette/src/dome/template/makefile b/ivette/src/dome/template/makefile
index 29df4121517ee94ea96a1a9e90a0ea3e559bd768..dee8d3b45167f7a2551ddfccb75dddea58c5438f 100644
--- a/ivette/src/dome/template/makefile
+++ b/ivette/src/dome/template/makefile
@@ -167,13 +167,6 @@ dome-reboot:
ifeq ("$(DOME)",".")
.gitignore:
@cp -f $(DOME)/template/git-ignore $@
-else
-.gitignore: $(DOME)/template/update.sh $(DOME)/template/git-ignore
- @((tail -r $(DOME)/template/git-ignore | tail -n +3 | tail -r) || head -n -3 $(DOME)/template/git-ignore) > $(DOME)/template/git-ignore.local
- @echo "/$(DOME)" >> $(DOME)/template/git-ignore.local
- @tail -2 $(DOME)/template/git-ignore >> $(DOME)/template/git-ignore.local
- @$^.local $@
- @rm -f $(DOME)/template/git-ignore.local
endif
.babelrc: $(DOME)/template/update.sh $(DOME)/template/babelrc.json
diff --git a/ivette/src/dome/template/package.sh b/ivette/src/dome/template/package.sh
index 5cadbb7444030b1dfb0cec0a82f6591554fe1bdd..e26dc01a53bb9220cbfd74cd74a8008b45e81590 100755
--- a/ivette/src/dome/template/package.sh
+++ b/ivette/src/dome/template/package.sh
@@ -1,4 +1,4 @@
-#!/bin/sh
+#! /usr/bin/env bash
##########################################################################
# #
# This file is part of Frama-C. #
diff --git a/ivette/src/dome/template/update.sh b/ivette/src/dome/template/update.sh
index d48e589170acc09d3e9bbb52e76d377912e51574..fd2dfbb918cf537e508f6ba361638fa709c706e9 100755
--- a/ivette/src/dome/template/update.sh
+++ b/ivette/src/dome/template/update.sh
@@ -1,4 +1,4 @@
-#!/bin/sh
+#! /usr/bin/env bash
##########################################################################
# #
# This file is part of Frama-C. #
diff --git a/ivette/yarn.lock b/ivette/yarn.lock
index 8a0f4ac205f03ce5b8717c7be06b409f8b8ec76b..1970b9068a63a7e38c8b05fee219a7fe345951b9 100644
--- a/ivette/yarn.lock
+++ b/ivette/yarn.lock
@@ -3282,15 +3282,10 @@ camelcase@^6.2.0:
resolved "https://registry.yarnpkg.com/camelcase/-/camelcase-6.2.1.tgz#250fd350cfd555d0d2160b1d51510eaf8326e86e"
integrity sha512-tVI4q5jjFV5CavAU8DXfza/TJcZutVKo/5Foskmsqcm0MsL91moHvwiGNnqaa2o6PF/7yT5ikDRcVcl8Rj6LCA==
-caniuse-lite@^1.0.30001280:
- version "1.0.30001286"
- resolved "https://registry.yarnpkg.com/caniuse-lite/-/caniuse-lite-1.0.30001286.tgz#3e9debad420419618cfdf52dc9b6572b28a8fff6"
- integrity sha512-zaEMRH6xg8ESMi2eQ3R4eZ5qw/hJiVsO/HlLwniIwErij0JDr9P+8V4dtx1l+kLq6j3yy8l8W4fst1lBnat5wQ==
-
-caniuse-lite@^1.0.30001313:
- version "1.0.30001314"
- resolved "https://registry.yarnpkg.com/caniuse-lite/-/caniuse-lite-1.0.30001314.tgz#65c7f9fb7e4594fca0a333bec1d8939662377596"
- integrity sha512-0zaSO+TnCHtHJIbpLroX7nsD+vYuOVjl3uzFbJO1wMVbuveJA0RK2WcQA9ZUIOiO0/ArMiMgHJLxfEZhQiC0kw==
+caniuse-lite@^1.0.30001280, caniuse-lite@^1.0.30001313:
+ version "1.0.30001422"
+ resolved "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001422.tgz"
+ integrity sha512-hSesn02u1QacQHhaxl/kNMZwqVG35Sz/8DgvmgedxSH8z9UUpcDYSPYgsj3x5dQNRcNp6BwpSfQfVzYUTm+fog==
catharsis@^0.9.0:
version "0.9.0"
diff --git a/opam/opam b/opam
similarity index 85%
rename from opam/opam
rename to opam
index 73a337edef9c7df53ff31ab401769c9f4b6ed1de..1c29e632b31b386ad30d765ebff74dc9630647a5 100644
--- a/opam/opam
+++ b/opam
@@ -96,6 +96,10 @@ install: [
[make "PREFIX=%{prefix}%" "-C" "doc" "install"] {with-doc}
]
+remove: [
+ [make "PREFIX=%{prefix}%" "-f" "ivette/Makefile.installation" "uninstall"]
+]
+
run-test: [
["dune" "exec" "--" "frama-c-ptests" "tests" "src/plugins/*/tests"
] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" }
@@ -138,5 +142,18 @@ depopts: [
]
post-messages: [
- "Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect"
+"The Frama-C/WP plug-in requires one or more external prover(s).
+Recommended provers are:
+- Alt-Ergo (https://alt-ergo.ocamlpro.com)
+- CVC4 (https://cvc4.github.io)
+- Z3 (https://github.com/Z3Prover/z3)
+Use 'why3 config detect' to configure new provers.
+Â "
+"Ivette is a new GUI for Frama-C, currently in development.
+Run 'ivette' once to finalize installation (requires an internet connection).
+Once finalized, 'ivette' will work offline.
+Finalization also requires Node v16 and Yarn:
+- install NVM (https://github.com/nvm-sh/nvm)
+- run 'nvm use 16'
+- run 'npm install --global yarn'"
]