add build manifest, improve build system
This commit is contained in:
zapashcanon
parent
96f8e6d4aa
commit
8aaabdd0e5
GPG Key ID:
8981C3C62D1D28F1
21
.build.yml
Normal file
21
.build.yml
Normal file
@ -0,0 +1,21 @@
|
||||
image: debian/unstable
|
||||
packages:
|
||||
- fonts-linuxlibertine
|
||||
- inkscape
|
||||
- python3-pygments
|
||||
- texlive-extra-utils
|
||||
- texlive-fonts-extra
|
||||
- texlive-lang-french
|
||||
- texlive-xetex
|
||||
sources:
|
||||
- https://git.zapashcanon.fr/zapashcanon/poster-jdse-2017
|
||||
secrets:
|
||||
- ec1f49cd-38dc-41d9-89f4-c3b6ecd7bcad # ssh deploy key
|
||||
tasks:
|
||||
- build: |
|
||||
cd poster-jdse-2017
|
||||
make
|
||||
ls main.pdf
|
||||
- deploy: |
|
||||
cd poster-jdse-2017
|
||||
scp -o StrictHostKeyChecking=no -q main.pdf fs@zapashcanon.fr:/var/www/fs.zapashcanon.fr/pdf/poster-jdse-2017.pdf
|
||||
3
.gitignore
vendored
Normal file
3
.gitignore
vendored
Normal file
@ -0,0 +1,3 @@
|
||||
*.aux
|
||||
*.log
|
||||
main.pdf
|
||||
@ -0,0 +1 @@
|
||||
# Poster JDSE 2017 [](https://builds.sr.ht/~zapashcanon/poster-jdse-2017?)
|
||||
@ -2,9 +2,12 @@
|
||||
|
||||
set -eu
|
||||
|
||||
( cd "$(dirname "$0")"/../
|
||||
( cd "$(dirname "$0")"/../src
|
||||
|
||||
xelatex -shell-escape src/poster-jdse-2017.tex
|
||||
xelatex -shell-escape src/poster-jdse-2017.tex
|
||||
xelatex -shell-escape src/poster-jdse-2017.tex
|
||||
)
|
||||
c="texfot xelatex -shell-escape -halt-on-error"
|
||||
|
||||
$c main.tex | sed '/Output written/d' | sed '/Rerun to get \/Page/d' | sed '/Warning: Citation/d' | sed '/Warning: Empty bib/d' | sed '/has changed/d' | sed '/Warning: There were/d' | sed '/biblatex Warning/d'
|
||||
$c main.tex | sed '/Output written/d' | sed '/Warning: There were/d' | sed '/biblatex Warning/d'
|
||||
$c main.tex
|
||||
mv main.pdf ../main.pdf
|
||||
) | sed '/This is/d' | sed '/texfot: invoking/d'
|
||||
|
||||
@ -9,11 +9,11 @@
|
||||
%----------------------------------------
|
||||
\documentclass[12pt]{scrartcl}
|
||||
|
||||
\input{src/packages.tex}
|
||||
\input{packages.tex}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\input{src/title.tex}
|
||||
\input{title.tex}
|
||||
|
||||
% Generate the poster header and footer
|
||||
\makeposter{}
|
||||
@ -25,12 +25,12 @@
|
||||
Until now there have been little usages of formal methods towards SQL and DBMS, yet, the compilation chain of SQL queries is complex.
|
||||
|
||||
\begin{figure}[h!]
|
||||
\caption{SQL's compilation chain}
|
||||
\label{sql-compil-chain}
|
||||
\centering
|
||||
\begin{center}
|
||||
\includegraphics[scale=1]{img/compilchain.pdf}\\
|
||||
\end{center}
|
||||
\caption{SQL's compilation chain}
|
||||
\label{sql-compil-chain}
|
||||
\centering
|
||||
\begin{center}
|
||||
\includegraphics[scale=1]{../img/compilchain.pdf}\\
|
||||
\end{center}
|
||||
\end{figure}
|
||||
|
||||
%Le poster est formatté avec LaTeX. Les instructions détaillées sont dans le fichier source et le source de ce poster peut servir d'exemple.
|
||||
@ -43,12 +43,12 @@ Until now there have been little usages of formal methods towards SQL and DBMS,
|
||||
|
||||
\section{Certified parsing, from SQL to SQLCoq}
|
||||
\inputminted[bgcolor=darkBackground]
|
||||
{sql}
|
||||
{src/query_14.sql}
|
||||
{sql}
|
||||
{query_14.sql}
|
||||
\begin{itemize}
|
||||
\item SQL parser in menhir/OCamllex
|
||||
\item certified using the CompCert parser generator
|
||||
\item automatic translation into SQLCoq (in OCaml)
|
||||
\item SQL parser in menhir/OCamllex
|
||||
\item certified using the CompCert parser generator
|
||||
\item automatic translation into SQLCoq (in OCaml)
|
||||
\end{itemize}
|
||||
% We parse SQL queries using the certified parser generator written by Jacques-Henri Jourdan and used in CompCert. At the end, we have an SQLCoq-compatible representation of the query. SQLCoq is a Coq library formalising SQL.
|
||||
|
||||
@ -69,8 +69,8 @@ Until now there have been little usages of formal methods towards SQL and DBMS,
|
||||
\section{Involving DBMS, from SQL to unified execution plan}
|
||||
|
||||
\begin{itemize}
|
||||
\item PostgreSQL and Oracle query execution plan parser
|
||||
\item both translated to our own unified plan format
|
||||
\item PostgreSQL and Oracle query execution plan parser
|
||||
\item both translated to our own unified plan format
|
||||
\end{itemize}
|
||||
%We give an SQL query to two DBMS (PostgreSQL and Oracle) and get the query execution plan, that is, the algorithms which are going to be used to fetch the data from the disk.
|
||||
|
||||
@ -93,8 +93,8 @@ Until now there have been little usages of formal methods towards SQL and DBMS,
|
||||
\threecolsection{From unified plan to Extended Algebra}
|
||||
%----------------------------------------
|
||||
\inputminted[bgcolor=lightBackground]
|
||||
{xml}
|
||||
{src/query_14.xml}
|
||||
{xml}
|
||||
{query_14.xml}
|
||||
|
||||
%Pour formatter le texte sur \emph{trois colonnes}, c'est le même principe que pour deux colonnes mais avec les commandes \verb|\threecolsection{<titre>}| et \verb|\threecoltext|.
|
||||
%Il faut bien sûr utiliser deux fois la commande \verb|\columnbreak| pour séparer les trois colonnes entre elles, et terminer avec \verb|\onecol|.
|
||||
@ -103,10 +103,10 @@ Until now there have been little usages of formal methods towards SQL and DBMS,
|
||||
%........................................
|
||||
|
||||
\begin{itemize}
|
||||
\item Extended Algebra (ExtAlg) is similar to Relationnal Algebra but more powerful
|
||||
\item translation from an unified plan to an ExtAlg expression
|
||||
\item automatic annotation of ExtAlg expression with algorithms
|
||||
\item ability to execute our Coq version of those algorithms
|
||||
\item Extended Algebra (ExtAlg) is similar to Relationnal Algebra but more powerful
|
||||
\item translation from an unified plan to an ExtAlg expression
|
||||
\item automatic annotation of ExtAlg expression with algorithms
|
||||
\item ability to execute our Coq version of those algorithms
|
||||
\end{itemize}
|
||||
|
||||
%Here, the expression is annotated with algorithms. Thus, we'll be able to go further by executing the algorithms which were formalized in Coq.
|
||||
@ -125,8 +125,8 @@ Until now there have been little usages of formal methods towards SQL and DBMS,
|
||||
%\end{center}
|
||||
%{\setmonofont{Everson Mono}
|
||||
\inputminted[bgcolor=darkBackground]
|
||||
{ocaml}
|
||||
{src/query_14.extalg}
|
||||
{ocaml}
|
||||
{query_14.extalg}
|
||||
%}
|
||||
|
||||
\onecol{}
|
||||
@ -136,9 +136,9 @@ Until now there have been little usages of formal methods towards SQL and DBMS,
|
||||
%----------------------------------------
|
||||
|
||||
\begin{itemize}
|
||||
\item translation from SQLCoq to ExtAlg
|
||||
\item two ExtAlg expressions, one from the DBMS, one from the SQL query/SQLCoq
|
||||
\item proof that two ExtAlg expression have the same semantic
|
||||
\item translation from SQLCoq to ExtAlg
|
||||
\item two ExtAlg expressions, one from the DBMS, one from the SQL query/SQLCoq
|
||||
\item proof that two ExtAlg expression have the same semantic
|
||||
\end{itemize}
|
||||
%Now we have the ExtAlg expression of the query from the plan the DBMS gave us. We also have the SQLCoq representation of the query. We can get the ExtAlg expression from the SQLCoq representation. We can show the equivalence of the two ExtAlg queries, by using normal forms on logical formulas, or using other Coq-proved equivalence on ExtAlg.
|
||||
%\begin{cbox}
|
||||
@ -154,9 +154,9 @@ Until now there have been little usages of formal methods towards SQL and DBMS,
|
||||
%........................................
|
||||
|
||||
\begin{itemize}
|
||||
\item strong guarantees about the fact that the DBMS kept the semantic of the SQL query
|
||||
\item algorithms used by the DBMS have not been proved yet
|
||||
\item Coq version of some algorithms
|
||||
\item strong guarantees about the fact that the DBMS kept the semantic of the SQL query
|
||||
\item algorithms used by the DBMS have not been proved yet
|
||||
\item Coq version of some algorithms
|
||||
\end{itemize}
|
||||
%With the equivalence of the two expressions, we are sure that the algorithms that the DMBS planned to use are corrects and that they won't change the semantic of the SQL query. We still have to prove that algorithms used in DBMS are correct, or to use our own written in Coq.
|
||||
|
||||
@ -3,7 +3,7 @@
|
||||
%\usepackage{isolatin1}
|
||||
|
||||
% [optional] Edit the line below with the path (absolute or relative) to the template directory
|
||||
\def\templatedir{.}
|
||||
\def\templatedir{./../}
|
||||
|
||||
% Include the LRI poster package
|
||||
\usepackage{\templatedir/includes/poster}
|
||||
@ -32,12 +32,12 @@
|
||||
\inrialogo{}
|
||||
|
||||
% xcolor
|
||||
\definecolor{darkBackground}{HTML}{282c34} % source code background
|
||||
\definecolor{darkBackgroundHighlight}{HTML}{2c323c} % source code background
|
||||
\definecolor{lightBackground}{HTML}{D7D3CB} % source code background
|
||||
\definecolor{darkBackground}{HTML}{282c34} % source code background
|
||||
\definecolor{darkBackgroundHighlight}{HTML}{2c323c} % source code background
|
||||
\definecolor{lightBackground}{HTML}{D7D3CB} % source code background
|
||||
|
||||
% source code
|
||||
\usepackage[cache=false, draft=false]{minted}
|
||||
\usemintedstyle{paraiso-dark}
|
||||
\setminted{bgcolor=lightBackground}
|
||||
\setminted{autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{9pt}{7pt}, frame=none, stepnumber=2}
|
||||
\usemintedstyle{paraiso-dark}
|
||||
\setminted{bgcolor=lightBackground}
|
||||
\setminted{autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{9pt}{7pt}, frame=none, stepnumber=2}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user