Commit edef4a01 authored by Frédéric Dabrowski's avatar Frédéric Dabrowski
Browse files

Domain semantics 0.1

parent 381e1840
\relax
\@writefile{toc}{\contentsline {section}{\numberline {1}Syntax}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {2}Dynamic semantics}{1}}
This is pdfTeX, Version 3.14159265-2.6-1.40.18 (TeX Live 2017/Debian) (preloaded format=pdflatex 2017.11.2) 5 FEB 2018 08:49
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**main.tex
(./main.tex
LaTeX2e <2017-04-15>
Babel <3.12> and hyphenation patterns for 84 language(s) loaded.
(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size12.clo
File: size12.clo 2014/09/29 v1.4h Standard LaTeX file (size option)
)
\c@part=\count79
\c@section=\count80
\c@subsection=\count81
\c@subsubsection=\count82
\c@paragraph=\count83
\c@subparagraph=\count84
\c@figure=\count85
\c@table=\count86
\abovecaptionskip=\skip41
\belowcaptionskip=\skip42
\bibindent=\dimen102
)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
Package: amssymb 2013/01/14 v3.01 AMS font symbols
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty
Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
\@emptytoks=\toks14
\symAMSa=\mathgroup4
\symAMSb=\mathgroup5
LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
(Font) U/euf/m/n --> U/euf/b/n on input line 106.
))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
Package: amsmath 2016/11/05 v2.16a AMS math features
\@mathmargin=\skip43
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
Package: amstext 2000/06/29 v2.01 AMS text
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty
File: amsgen.sty 1999/11/30 v2.0 generic functions
\@emptytoks=\toks15
\ex@=\dimen103
))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d Bold Symbols
\pmbraise@=\dimen104
)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty
Package: amsopn 2016/03/08 v2.02 operator names
)
\inf@bad=\count87
LaTeX Info: Redefining \frac on input line 213.
\uproot@=\count88
\leftroot@=\count89
LaTeX Info: Redefining \overline on input line 375.
\classnum@=\count90
\DOTSCASE@=\count91
LaTeX Info: Redefining \ldots on input line 472.
LaTeX Info: Redefining \dots on input line 475.
LaTeX Info: Redefining \cdots on input line 596.
\Mathstrutbox@=\box26
\strutbox@=\box27
\big@size=\dimen105
LaTeX Font Info: Redeclaring font encoding OML on input line 712.
LaTeX Font Info: Redeclaring font encoding OMS on input line 713.
\macc@depth=\count92
\c@MaxMatrixCols=\count93
\dotsspace@=\muskip10
\c@parentequation=\count94
\dspbrk@lvl=\count95
\tag@help=\toks16
\row@=\count96
\column@=\count97
\maxfields@=\count98
\andhelp@=\toks17
\eqnshift@=\dimen106
\alignsep@=\dimen107
\tagshift@=\dimen108
\tagwidth@=\dimen109
\totwidth@=\dimen110
\lineht@=\dimen111
\@envbody=\toks18
\multlinegap=\skip44
\multlinetaggap=\skip45
\mathdisplay@stack=\toks19
LaTeX Info: Redefining \[ on input line 2817.
LaTeX Info: Redefining \] on input line 2818.
) (./main.aux)
\openout1 = `main.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 5.
LaTeX Font Info: ... okay on input line 5.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 5.
LaTeX Font Info: ... okay on input line 5.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 5.
LaTeX Font Info: ... okay on input line 5.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 5.
LaTeX Font Info: ... okay on input line 5.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 5.
LaTeX Font Info: ... okay on input line 5.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 5.
LaTeX Font Info: ... okay on input line 5.
LaTeX Font Info: Try loading font information for U+msa on input line 6.
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd
File: umsa.fd 2013/01/14 v3.01 AMS symbols A
)
LaTeX Font Info: Try loading font information for U+msb on input line 6.
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
)
LaTeX Warning: No \author given.
Overfull \hbox (37.0317pt too wide) detected at line 120
[]
[]
[1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2] (./main.aux) )
Here is how much of TeX's memory you used:
1164 strings out of 492990
12798 string characters out of 6135005
77827 words of memory out of 5000000
4757 multiletter control sequences out of 15000+600000
13342 words of font info for 52 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
27i,23n,26p,215b,203s stack positions out of 5000i,500n,10000p,200000b,80000s
</usr/sh
are/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfo
nts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/
cmti12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12
.pfb>
Output written on main.pdf (2 pages, 95977 bytes).
PDF statistics:
51 PDF objects out of 1000 (max. 8388607)
36 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000)
\documentclass[12pt]{article}
\usepackage{amssymb}
\usepackage{amsmath}
\title{ocamlmc}
\usepackage{stmaryrd}
\usepackage{MnSymbol}
\title{Draft Semantics of OCaml Multicore Domains}
\date{}
\begin{document}
\maketitle
\newcommand{\alloc}{{\tt{ref}}}
......@@ -22,101 +25,173 @@
\newcommand{\unit}{{\mathit{unit}}}
\newcommand{\fix}{{\tt{fix}}}
\newcommand{\constant}{{\mathit{constant}}}
\newcommand{\val}{{\mathit{value}}}
\newcommand{\heap}{{\mathit{heap}}}
\newcommand{\pool}{{\mathit{pool}}}
\newcommand{\expression}{{\mathit{expression}}}
\newcommand{\name}{{\mathit{domain}}}
\newcommand{\location}{{\mathit{location}}}
\newcommand{\csem}[2]{\llparenthesis #1\rrparenthesis_{#2}}
\section{Syntax}
We consider a polymorphic $\lambda$-calculus extended with memory locations of type $\alpha~\reference$,
domain names of type $\alpha~\domain$ and the following
We consider a polymorphic $\lambda$-calculus extended with the following
constants
$$
\begin{array}{cc}
\begin{array}{lcl}
\fix &:& (\alpha \rightarrow \alpha) \rightarrow \alpha\\
() &:& \unit\\
\alloc &:& \alpha \rightarrow \alpha~\reference\\
\get &:& \alpha~\reference \rightarrow \alpha\\
\set &:& \alpha~\reference \rightarrow \alpha \rightarrow \unit
\fix &::& \forall \alpha.(\alpha \rightarrow \alpha) \rightarrow \alpha\\
() &::& \unit\\
\alloc &::& \forall \alpha.\alpha \rightarrow \alpha~\reference\\
\get &::& \forall \alpha.\alpha~\reference \rightarrow \alpha\\
\set &::& \forall \alpha.\alpha~\reference \rightarrow \alpha \rightarrow \unit
\end{array}
&
\begin{array}{lcl}
\spawn &:& (\unit \rightarrow \alpha) \rightarrow \alpha~\domain\\
\join &:& \alpha~\domain \rightarrow \alpha\\
\critical &:& (\unit \rightarrow \alpha) \rightarrow \alpha\\
\notify &:& '\alpha~{\mathit{\domain}} \rightarrow \unit\\
\wait &:& \unit \rightarrow \unit
\spawn &::& \forall \alpha.(\unit \rightarrow \alpha) \rightarrow \alpha~\domain\\
\join &::& \forall \alpha.\alpha~\domain \rightarrow \alpha\\
\critical &::& \forall \alpha.(\unit \rightarrow \alpha) \rightarrow \alpha\\
\notify &::& \forall \alpha.\alpha~{\mathit{\domain}} \rightarrow \unit\\
\wait &::& \unit \rightarrow \unit
\end{array}
\end{array}
$$
where types are defines as follows:
$$
\begin{array}{lcl}
c &::=& a \mid d \mid \alloc \mid \get \mid \set \mid \spawn \mid \join \mid \critical \mid \wait \mid \notify\\
e &::=& c \mid x \mid \lambda x . e \mid e~ e
\begin{array}{lcll}
\tau &::=& \alpha \mid \unit \mid \name \mid \tau~ref \mid \tau \rightarrow \tau \mid \forall \alpha.\tau
& {\text{(types)}}
\end{array}
$$
\section{Dynamic semantics}
$$
\overline{\critical} : \alpha \rightarrow \alpha
$$
Expressions are defined as follows:
$$
\begin{array}{lcl}
c &::=& \ldots \mid \overline{\critical}\\
v &::=& c \mid \set~v \mid \lambda x .e\\
C &::=& [] \mid C~e \mid v~C
\begin{array}{lcll}
c &::=& \alloc \mid \get \mid \set \mid \spawn \mid \join \mid \critical \mid \wait \mid \notify
& {\text{(constants)}}\\
e &::=& c \mid x \mid \lambda x . e \mid e~ e& {\text{(expressions)}}
\end{array}
$$
% $$
% \begin{array}{c}
% \cfrac{c :: \tau}{\Gamma \vdash c:\tau}
% \qquad
% \cfrac{}{\Gamma,x :\tau \vdash x :\tau}
% \qquad
% \cfrac{\Gamma \vdash e: \forall \alpha.\tau}
% {\Gamma \vdash e : \tau[\tau'/\alpha]}
% \\\\
% \cfrac{\Gamma, x:\tau_1 \vdash e:\tau_2}{\Gamma \vdash \lambda x.e : \tau_1 \rightarrow \tau_2}
% \qquad
% \cfrac{
% \Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \qquad \Gamma \vdash e_2 : \tau_1
% }{
% \Gamma \vdash e_1~e_2 : \tau_2
% }
% \end{array}
% $$
\section{Dynamic semantics}
We extend constants with memory locations $\location$,
domain names $\domain$ and special constants
$\set~\ell$ and $\overline{\critical}:\forall \alpha.\alpha \rightarrow \alpha$.
Intuitively, $\set~\ell$ is the result of the partial application of $\set$ to $\ell$
The type of locations, domain names and of the partial application $\set~\ell$ is
run-time dependent.
The function $\overline{\critical} :: \forall \alpha.\alpha \rightarrow \alpha$
closes a critical section and returns its parameter.
$$
\begin{array}{lcl}
\watching(T,t) &=& \pi_2(T(t)) = \bullet\\
\notified(T,t) &=& \exists C,t'.\pi_2(T(t')) = C[\notify~t]\\
\suspended(T,t) &=& \exists C.T(t) = (C[\wait],\bullet)\\
\terminated(T,t,v) &=& T(t) = v
\begin{array}{lclcll}
constant &\owns& c &::=& \ldots \mid \ell \mid \set~\ell \mid t \mid\overline{\critical}
\ell \in \location, t \in \domain\\
value &\owns&v &::=& c \mid \lambda x .e\\
context &\owns&C &::=& [] \mid C~e \mid v~C
\end{array}
$$
The semantics is defined as a reduction relation. A state if a pair $(T,\sigma)$ where
$$
\begin{array}{lcll}
T &:& \name \rightharpoonup \expression & {\text{(pool)}}\\
\sigma &:& \location \rightharpoonup \val & {\text{(heap)}}
\end{array}
$$
Given a function $F:A \rightarrow B$, and elements $x \in A$ and $e \in B$,
we note $F[x \mapsto v]$ the function defined by
$$
\sigma[\ell \mapsto v] = (\sigma \setminus \{(\ell,v') \mid v' \in V\}) \uplus \{(\ell,v)\}
\sigma[\ell \mapsto v] \triangleeq
(\sigma \setminus \{(\ell,v') \mid v' \in V\}) \uplus \{(\ell,v)\}
$$
To define the reduction rules we need to define some properties over thread pools.
\begin{itemize}
\item $\watching(T,t)$ holds if domain $t$ is in a critical section
$$\watching(T,t) \triangleeq \exists C,e.T(t) = C[\overline{\critical}~e]$$
\item $\notified(T,t)$ holds if domain $t$ is notified
$$\notified(T,t) \triangleeq \exists C,t'.T(t') = C[\notify~t]$$
\item $\suspended(T,t)$ holds if domain $t$ is suspended on a call to $\wait$
$$\suspended(T,t) \triangleeq \watching(T,t) \wedge \exists C.T(t) = C[\wait~()]$$
\item $\terminated(T,t,v)$ states that domain $t$ has terminated with value $v$
$$\terminated(T,t,v) \triangleeq T(t) = v$$
\end{itemize}
\noindent For all constant $c$ and domain $t$, we define the partial function
$$
\csem{c}{t} : (\val \times \heap \times \pool)
\rightarrow (\expression \times \heap \times \pool)
$$
Intuivitly $\csem{c}{t}(v,\sigma,T)$ denotes a call to $c$ applied to $v$ in context formed
by heap $\sigma$ and pool $T$. It produces a triple $(e,\sigma',T')$ resulting from
this call where $e$ is the result of the call and $\sigma'$ and $T'$ are the new heap and pool produces by this call.
$$
\begin{array}{c}
\begin{array}{lcll}
T, t \vdash ((\lambda x.e)~v,s, \sigma) &\xrightarrow{\emptyset}& (e[v/x],s, \sigma)&
\\
T,t \vdash (\fix~(\lambda x.e), s, \sigma) &\xrightarrow{\emptyset}& , (e[\fix~(\lambda x.e) / x],s,\sigma)
\csem{\alloc}{t}(v,\sigma,T) &=& (\ell,\sigma[\ell \mapsto v]) & {\text{if }}\ell \not \in \dom(\sigma)
\\
T,t \vdash (\alloc~v,s,\sigma) &\xrightarrow{\emptyset} &(\ell,s,\sigma\uplus \{(\ell,v)\})&{\text{if }}\ell \not \in \dom(\sigma)\\
T,t \vdash (\get~\ell,s,\sigma) &\xrightarrow{\emptyset}&(v,s,\sigma) &{\text{if }}\sigma(\ell) = v
\csem{\get}{t}(\ell,\sigma,T) &=& (v,\sigma,T)&{\text{if }}\sigma(\ell) = v
\\
T,t \vdash (\set~\ell~v,s,\sigma) &\xrightarrow{\emptyset}& ((),s,\sigma[\ell \mapsto v]) &{\text{if }}\ell \in \dom(\sigma)
\csem{\set~\ell}{t}(v,\sigma,T)&=& ((),\sigma[\ell \mapsto v],T) &{\text{if }}\ell \in \dom(\sigma)
\\
T,t \vdash (\spawn~v, s,\sigma) &\xrightarrow{\{(d,v)\}}& (d,s, \sigma)& d \not \in \dom(T)
\csem{\spawn}{t}(v,\sigma,T) &=& (t', \sigma, T[d \mapsto v~()])& t' \not \in \dom(T)
\\
T,t \vdash (\join~t,s, \sigma) &\xrightarrow{\emptyset}&(v,s,\sigma) & {\text{if }} {\mathit{terminated}}(T,t,v)
\csem{\join}{t}(t', \sigma, T) &=&(v,s,\sigma) & {\text{if }} {\mathit{terminated}}(T,t,v)
\\
T,t \vdash (\critical~v,\circ,\sigma) &\xrightarrow{\emptyset}& (\overline{\critical}~(v~()),\bullet,\sigma)&
\csem{\critical}{t}(v,\circ,\sigma,T) &=& (\overline{\critical}~(v~()),\sigma,T)& {\text{if }} \neg \watching(T,t)
\\
T,t \vdash (\critical~v,\bullet,\sigma) &\xrightarrow{\emptyset}& ((v~()),\bullet,\sigma)&
\csem{\critical}{t}(v,\sigma,T) &=& (v~(),\sigma,T)& {\text{if }} \watching(T,t)
\\
T,t \vdash (\overline{\critical}~v,\bullet,\sigma) &\xrightarrow{\emptyset}& (v,\circ,\sigma)&
\csem{\overline{\critical}}{t}(v,\sigma,T) &=& (v,\sigma,T)&
\\
T,t \vdash (\wait~(),\bullet,\sigma) &\xrightarrow{\emptyset}& ((),\bullet,\sigma)&{\text{if }} {\mathit{\notified}}(T,t)
\csem{\wait}{t}((),\sigma,T) &=& ((),\sigma,T)&{\text{if }}
{\mathit{\watching}}(T,t) {\text{ and }} {\mathit{\notified}}(T,t)
\\
T,t \vdash (\notify~t',s,\sigma) &\xrightarrow{\emptyset} & ((), s, \sigma)&{\text{if }} \neg({\mathit{\watching}}(T,t'))
\end{array}\\\\
\csem{\notify}{t}(t',\sigma,T) &=& ((), \sigma,T)&{\text{if }} \neg({\mathit{\watching}}(T,t'))
\end{array}
\end{array}
$$
Finally the reduction relation is defined by rule $(red)$ given below. It relies on the reduction of redex as defined by rules ($\beta$-reduction) and (external).
$$
\begin{array}{cl}
((\lambda x.e)~v, \sigma, T) \rightarrow_t ((e[v/x],s), \sigma, T)
& {\text{($\beta$-reduction)}}
\\\\
\cfrac{
\llparenthesis c \rrparenthesis_t (v, \sigma,T) = (e,\sigma',T')
}
{
(c~v, \sigma,T) \rightarrow_t (e,\sigma',T')
}
& {\text{(external)}}
\\\\
\cfrac{
\begin{array}{c}
T(t) = (C[e],s) \qquad
T,t\vdash (e, s, \sigma) \xrightarrow{E} (e',s',\sigma') \\
T' = T[t \mapsto (C[e'],s')] \uplus \{(d,(v~(), \circ)) \mid (d,v) \in E\}
T(t) = C[e] \qquad
(e, \sigma,T) \rightarrow_t (e',\sigma',T') \\
\end{array}
}{
(T,\sigma) \rightarrow (T',\sigma')
(T,\sigma) \rightarrow (T'[t \mapsto C[e']] ,\sigma')
}
\end{array}
& {\text{(reduction)}}
\end{array}
$$
\end{document}
\ No newline at end of file
\documentclass[12pt]{article}
\usepackage{amssymb}
\usepackage{amsmath}
\begin{document}
\newcommand{\alloc}{\tt{ref}}
\newcommand{\spawn}{\tt{spawn}}
\newcommand{\critical}{\tt{critical}}
\newcommand{\wait}{\tt{wait}}
\newcommand{\notify}{\tt{notify}}
$$
\begin{array}{lcl}
e &::=&
x \mid \lambda x . e \mid e~ e \mid \alloc~e \mid {!e} \mid e:=e
\mid \spawn~e \mid \critical~e \mid \wait \mid \notify~e
\end{array}
$$
\end{document}
\ No newline at end of file
Require Import EquivDec.
Module Type Environment.
Parameter t : Set -> Set -> Set.
Section A.
Variable A : Set.
Variable B : Set.
Declare Instance tt : EqDec A (@eq A).
Parameter empty : t A B.
Parameter get : t A B -> A -> option B.
Parameter singleton : A -> B -> t A B.
Parameter dom : t A B -> list A.
Parameter update : t A B -> A -> B -> t A B.
End A.
Arguments get [A B] _ _.
Arguments update [A B] _ _.
Arguments dom [A B] _.
Notation "E '[' x '<-' v ']'" := (update E x v)
(at level 65, left associativity).
End Environment.
\ No newline at end of file
#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.6 ##
#############################################################################
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
#
# This Makefile was generated by the command line :
# coq_makefile -f _CoqProject
#
.DEFAULT_GOAL := all
# This Makefile may take arguments passed as environment variables:
# COQBIN to specify the directory where Coq binaries resides;
# TIMECMD set a command to log .v compilation time;
# TIMED if non empty, use the default time command as TIMECMD;
# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
# DSTROOT to specify a prefix to install path.
# VERBOSE to disable the short display of compilation rules.
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
# Here is a hack to make $(eval $(shell works:
define donewline
endef
includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
$(call includecmdwithout@,$(COQBIN)coqtop -config)
TIMED?=
TIMECMD?=
STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
vo_to_obj = $(addsuffix .o,\
$(filter-out Warning: Error:,\
$(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
##########################
# #
# Libraries definitions. #
# #
##########################
COQLIBS?=\
-R "." OCamlMC
COQCHKLIBS?=\
-R "." OCamlMC
COQDOCLIBS?=\
-R "." OCamlMC
##########################
# #
# Variables definitions. #
# #
##########################
OPT?=
COQDEP?="$(COQBIN)coqdep" -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
COQC?=$(TIMER) "$(COQBIN)coqc"
GALLINA?="$(COQBIN)gallina"
COQDOC?="$(COQBIN)coqdoc"
COQCHK?="$(COQBIN)coqchk"
COQMKTOP?="$(COQBIN)coqmktop"
##################
# #
# Install Paths. #
# #
##################
ifdef USERINSTALL
XDG_DATA_HOME?="$(HOME)/.local/share"
COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else
COQLIBINSTALL="${COQLIB}user-contrib"
COQDOCINSTALL="${DOCDIR}user-contrib"
COQTOPINSTALL="${COQLIB}toploop"
endif
######################
# #
# Files dispatching. #
# #
######################
VFILES:=Environment.v\
Syntax.v
ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(VFILES))
else
ifeq ($(MAKECMDGOALS),)
-include $(addsuffix .d,$(VFILES))
endif
endif
.SECONDARY: $(addsuffix .d,$(VFILES))
VO=vo
VOFILES:=$(VFILES:.v=.$(VO))
GLOBFILES:=$(VFILES:.v=.glob)
GFILES:=$(VFILES:.v=.g)
HTMLFILES:=$(VFILES:.v=.html)
GHTMLFILES:=$(VFILES:.v=.g.html)
OBJFILES=$(call vo_to_obj,$(VOFILES))
ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
ifeq '$(HASNATDYNLINK)' 'true'
HASNATDYNLINK_OR_EMPTY := yes
else
HASNATDYNLINK_OR_EMPTY :=
endif
#######################################
# #
# Definition of the toplevel targets. #
# #
#######################################