Commit 774b232a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Update release script to handle coq-menhirlib.

parent 33561435
Pipeline #64075 passed with stages
in 25 seconds
......@@ -143,10 +143,11 @@ release:
# Remove subdirectories that do not need to (or must not) be distributed.
@ make --quiet -C test clean
@ make --quiet -C quicktest clean
@ make --quiet -C coq-menhirlib clean
@ git rm -rf attic headers quicktest releases src/attic test --quiet
# Remove files that do not need to (or must not) be distributed.
# Keep check-tarball.sh because it is used below.
@ git rm GNUmakefile HOWTO.md TODO* menhir.opam --quiet
@ git rm GNUmakefile HOWTO.md TODO* *.opam --quiet
# Hardcode the version number in the files that mention it. These
# include version.ml, StaticVersion.{ml,mli}, version.tex, META.
@ echo let version = \"$(DATE)\" > src/version.ml
......@@ -243,8 +244,18 @@ export:
# This entry assumes that [make release] has been run on the same day.
# You need a version of opam-publish that supports --subdirectory:
# git clone git@github.com:fpottier/opam-publish.git
# cd opam-publish
# git checkout 1.3
# opam pin add opam-publish `pwd` -k git
# The following command should have been run once:
# opam publish repo add opam-coq-archive coq/opam-coq-archive
# The package name.
THIS := menhir
THIS_COQ_MENHIRLIB := coq-menhirlib
# The repository URL (https).
REPO := https://gitlab.inria.fr/fpottier/$(THIS)
......@@ -252,10 +263,16 @@ REPO := https://gitlab.inria.fr/fpottier/$(THIS)
# The archive URL (https).
ARCHIVE := $(REPO)/repository/$(DATE)/archive.tar.gz
# Additional options for coq-menhirlib
COQ_MENHIRLIB_PUBLISH_OPTIONS := \
--repo opam-coq-archive \
--subdirectory released \
.PHONY: opam
opam:
# Publish an opam description.
@ opam publish -v $(DATE) $(THIS) $(ARCHIVE) .
@ opam publish -v $(DATE) $(COQ_MENHIRLIB_PUBLISH_OPTIONS) $(THIS_COQ_MENHIRLIB) $(ARCHIVE) .
# -------------------------------------------------------------------------
......@@ -263,7 +280,7 @@ opam:
.PHONY: pin
pin:
opam pin add menhir .
opam pin add menhir.dev .
.PHONY: unpin
unpin:
......
......@@ -15,6 +15,13 @@ For manual installation, see [INSTALLATION.md](INSTALLATION.md).
Some instructions for developers can be found in [HOWTO.md](HOWTO.md).
## The Coq backend support library coq-menhirlib
The support library for the Coq backend of Menhir can be found in the
coq-menhirlib directory. It can be installed using
`opam install coq-menhirlib`, when the opam Coq "released" repository
is set up.
## Authors
* [François Pottier](Francois.Pottier@inria.fr)
......
......@@ -32,6 +32,7 @@ fi
TEMPDIR=`mktemp -d /tmp/menhir-test.XXXXXX`
INSTALL=$TEMPDIR/install
COQCONTRIB=$INSTALL/coq-contrib
cp $TARBALL $TEMPDIR
......@@ -42,7 +43,9 @@ echo " * Compiling and installing."
mkdir $INSTALL
(cd $TEMPDIR/$PACKAGE &&
make PREFIX=$INSTALL USE_OCAMLFIND=true &&
make PREFIX=$INSTALL USE_OCAMLFIND=true install
make PREFIX=$INSTALL USE_OCAMLFIND=true install &&
make -C coq-menhirlib all &&
make -C coq-menhirlib CONTRIB=$COQCONTRIB install
) > $TEMPDIR/install.log 2>&1 || (cat $TEMPDIR/install.log; exit 1)
echo " * Building the demos."
......@@ -53,6 +56,7 @@ echo " * Building the demos."
echo " * Uninstalling."
(cd $TEMPDIR/$PACKAGE &&
make PREFIX=$INSTALL USE_OCAMLFIND=true uninstall
make -C coq-menhirlib CONTRIB=$COQCONTRIB uninstall
) > $TEMPDIR/uninstall.log 2>&1 || (cat $TEMPDIR/uninstall.log; exit 1)
rm -rf $TEMPDIR
name: "coq-menhirlib"
opam-version: "1.2"
opam-version: "2.0"
synopsis: "A support library for verified Coq parsers produced by Menhir"
maintainer: "francois.pottier@inria.fr"
authors: [
"Jacques-Henri Jourdan <jacques-henri.jourdan@lri.fr>"
]
homepage: "https://gitlab.inria.fr/fpottier/coq-menhirlib"
dev-repo: "https://gitlab.inria.fr/fpottier/coq-menhirlib.git"
dev-repo: "git+https://gitlab.inria.fr/fpottier/menhir.git"
bug-reports: "jacques-henri.jourdan@lri.fr"
build: [
[make "-j%{jobs}%"]
[make "-C" "coq-menhirlib" "-j%{jobs}%"]
]
install: [
[make "install"]
[make "-C" "coq-menhirlib" "install"]
]
remove: [
[make "uninstall"]
[make "-C" "coq-menhirlib" "uninstall"]
]
depends: [
"coq" { >= "8.6" }
]
conflicts: [
"menhir" { < "20180530" }
"menhir" { = "dev" }
]
# -------------------------------------------------------------------------
# Private Makefile for package maintenance.
SHELL := bash
export CDPATH=
.PHONY: package export opam submit pin unpin
# -------------------------------------------------------------------------
include Makefile
# -------------------------------------------------------------------------
# Distribution.
# The version number is automatically set to the current date,
# unless DATE is defined on the command line.
DATE := $(shell /bin/date +%Y%m%d)
# The project name on gitlab.
PROJECT := coq-menhirlib
# The opam package name.
PACKAGE := coq-menhirlib
# The repository URL (https).
REPO := https://gitlab.inria.fr/fpottier/$(PROJECT)
# The archive URL (https).
ARCHIVE := $(REPO)/repository/$(DATE)/archive.tar.gz
# The local repository directory.
PWD := $(shell pwd)
# -------------------------------------------------------------------------
# Prepare a release.
package:
# Make sure the correct version can be installed.
@ make uninstall
@ make clean
@ make install
# -------------------------------------------------------------------------
# Publish a release. (Remember to commit everything first!)
export:
# Check if everything has been committed.
@ if [ -n "$$(git status --porcelain)" ] ; then \
echo "Error: there remain uncommitted changes." ; \
git status ; \
exit 1 ; \
else \
echo "Now making a release..." ; \
fi
# Create a git tag.
@ git tag -a $(DATE) -m "Release $(DATE)."
# Upload. (This automatically makes a .tar.gz archive available on gitlab.)
@ git push
@ git push --tags
# -------------------------------------------------------------------------
# Updating the opam package.
# This entry assumes that "make package" and "make export"
# have just been run (on the same day).
# You need opam-publish:
# sudo apt-get install libssl-dev
# opam install tls opam-publish
# In fact, you need a version of opam-publish that supports --subdirectory:
# git clone git@github.com:fpottier/opam-publish.git
# cd opam-publish
# git checkout 1.3
# opam pin add opam-publish `pwd` -k git
# The following command should have been run once:
# opam-publish repo add opam-coq-archive coq/opam-coq-archive
PUBLISH_OPTIONS := \
--repo opam-coq-archive \
--subdirectory released \
opam:
@ opam lint
@ opam-publish prepare $(PUBLISH_OPTIONS) $(PACKAGE).$(DATE) $(ARCHIVE)
submit:
@ opam-publish submit $(PUBLISH_OPTIONS) $(PACKAGE).$(DATE)
# -------------------------------------------------------------------------
# Pinning.
pin:
opam pin add $(PACKAGE) `pwd` -k git
unpin:
opam pin remove $(PACKAGE)
......@@ -3964,8 +3964,8 @@ library. This library can be installed via the command \verb+opam install coq-me
and that you have run the command \texttt{opam repo add coq-released
https://coq.inria.fr/opam/released}.}
%
The Coq sources of this library can be found at
\url{https://gitlab.inria.fr/fpottier/coq-menhirlib}.
The Coq sources of this library can be found in
the \texttt{coq-menhirlib} directory of the Menhir repository.
The CompCert verified compiler~\cite{compcert,compcert-github} can be used as
an example if one wishes to use \menhir to generate a formally verified parser
......@@ -3987,6 +3987,9 @@ Extract Constant Int31.In => "1".
\end{comment}
% Peut-être en faire aussi un fichier de librairie?
% jh : Ce ne devrait plus être nécessaire aujourd'hui, puisque les
% int31 ne sont plus utilisés à runtime.
% ------------------------------------------------------------------------------
\section{Building grammarware on top of \menhir}
......
Markdown is supported
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