l3-ENSL/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

avancement du rapport

Browse Source
This commit is contained in:
Marwan 2024-05-14 11:41:37 +02:00
parent 5ecf82920f
commit 3bb8efcb8f
10 changed files with 713 additions and 182 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
RapportPresentation/ex-biblio.bib
View File

@ -16,3 +16,14 @@
editor = {Eddy Caron} editor = {Eddy Caron}
} }
@article{SelingerNotes,
author = {Peter Selinger},
title = {Lecture notes on the lambda calculus},
journal = {CoRR},
year = {2008},
url = {http://arxiv.org/abs/0804.3434},
eprinttype = {arXiv},
timestamp = {Mon, 13 Aug 2018 16:48:04 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0804-3434.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

25
RapportPresentation/ex-rapport.aux
View File

@ -1,10 +1,23 @@
\relax \relax
\citation{ProjInt16} \providecommand\babel@aux[2]{}
\@nameuse{bbl@beforestart}
\catcode `:\active
\catcode `;\active
\catcode `!\active
\catcode `?\active
\babel@aux{french}{}
\@writefile{toc}{\contentsline {section}{\numberline {1}Présentation}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {1}Présentation}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {2}Organisation du code}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {2}Compiler et exécuter}{1}{}\protected@file@percent }
\newlabel{s:orga}{{2}{1}{}{}{}} \newlabel{s:opt}{{2}{1}{}{}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Critique des performances}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {3}Organisation du code}{1}{}\protected@file@percent }
\newlabel{s:orga}{{3}{1}{}{}{}}
\citation{SelingerNotes}
\bibstyle{plain} \bibstyle{plain}
\bibdata{ex-biblio} \bibdata{ex-biblio}
\bibcite{ProjInt16}{1} \bibcite{SelingerNotes}{1}
\gdef \@abspage@last{2} \@writefile{toc}{\contentsline {section}{\numberline {4}$\lambda $-calcul simplement typé}{2}{}\protected@file@percent }
\newlabel{s:stlc}{{4}{2}{}{}{}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Preuves}{2}{}\protected@file@percent }
\newlabel{s:proof}{{5}{2}{}{}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Vérification des preuves}{2}{}\protected@file@percent }
\gdef \@abspage@last{3}

8
RapportPresentation/ex-rapport.bbl
View File

@ -1,8 +1,8 @@
\begin{thebibliography}{1} \begin{thebibliography}{1}
\bibitem{ProjInt16} \bibitem{SelingerNotes}
Les~M1 du~DI. Peter Selinger.
\newblock Notre beau projet intégré. \newblock Lecture notes on the lambda calculus.
\newblock In Eddy Caron, editor, {\em Recueil des projets intégrés de l'année}, volume~1 of {\em Best sellers du DI}, pages 10--22. ENS de Lyon, 2016. \newblock {\em CoRR}, 2008.
\end{thebibliography} \end{thebibliography}

44
RapportPresentation/ex-rapport.blg
View File

@ -5,42 +5,42 @@ The style file: plain.bst
Database file #1: ex-biblio.bib Database file #1: ex-biblio.bib
You've used 1 entry, You've used 1 entry,
2118 wiz_defined-function locations, 2118 wiz_defined-function locations,
509 strings with 4174 characters, 503 strings with 4086 characters,
and the built_in function-call counts, 453 in all, are: and the built_in function-call counts, 224 in all, are:
= -- 45 = -- 20
> -- 11 > -- 7
< -- 2 < -- 0
+ -- 4 + -- 3
- -- 3 - -- 2
* -- 31 * -- 10
:= -- 72 := -- 48
add.period$ -- 4 add.period$ -- 3
call.type$ -- 1 call.type$ -- 1
change.case$ -- 4 change.case$ -- 4
chr.to.int$ -- 0 chr.to.int$ -- 0
cite$ -- 1 cite$ -- 1
duplicate$ -- 22 duplicate$ -- 10
empty$ -- 41 empty$ -- 18
format.name$ -- 3 format.name$ -- 2
if$ -- 101 if$ -- 42
int.to.chr$ -- 0 int.to.chr$ -- 0
int.to.str$ -- 1 int.to.str$ -- 1
missing$ -- 1 missing$ -- 1
newline$ -- 8 newline$ -- 8
num.names$ -- 4 num.names$ -- 2
pop$ -- 5 pop$ -- 4
preamble$ -- 1 preamble$ -- 1
purify$ -- 3 purify$ -- 3
quote$ -- 0 quote$ -- 0
skip$ -- 16 skip$ -- 7
stack$ -- 0 stack$ -- 0
substring$ -- 29 substring$ -- 5
swap$ -- 11 swap$ -- 1
text.length$ -- 2 text.length$ -- 0
text.prefix$ -- 0 text.prefix$ -- 0
top$ -- 0 top$ -- 0
type$ -- 4 type$ -- 4
warning$ -- 0 warning$ -- 0
while$ -- 6 while$ -- 2
width$ -- 2 width$ -- 2
write$ -- 15 write$ -- 12

122
RapportPresentation/ex-rapport.fdb_latexmk
View File

@ -1,54 +1,84 @@
# Fdb version 4 # Fdb version 4
["bibtex ex-rapport"] 1715617052.40433 "ex-rapport.aux" "ex-rapport.bbl" "ex-rapport" 1715617081.68301 0 ["bibtex ex-rapport"] 1715673124.42722 "ex-rapport.aux" "ex-rapport.bbl" "ex-rapport" 1715675326.19747 0
"./ex-biblio.bib" 1493037286 435 eb384d654794ae20bc01965f6b4e4822 "" "./ex-biblio.bib" 1715672341.14715 878 b24a3ee5eaad1f378a00844cfb93a00b ""
"/usr/share/texmf-dist/bibtex/bst/base/plain.bst" 1711186958 20613 bd3fbfa9f64872b81ac57a0dd2ed855f "" "/usr/share/texmf-dist/bibtex/bst/base/plain.bst" 1713199481 20613 bd3fbfa9f64872b81ac57a0dd2ed855f ""
"ex-rapport.aux" 1715617081.51618 467 dfd15de10c0a5a19b1ec96e1b8771110 "pdflatex" "ex-rapport.aux" 1715675325.91528 1056 73909169f0984220be1f002f5c1fdca4 "pdflatex"
(generated) (generated)
"ex-rapport.bbl" "ex-rapport.bbl"
"ex-rapport.blg" "ex-rapport.blg"
(rewritten before read) (rewritten before read)
["pdflatex"] 1715617081.286 "ex-rapport.tex" "ex-rapport.pdf" "ex-rapport" 1715617081.6834 0 ["pdflatex"] 1715675325.3409 "ex-rapport.tex" "ex-rapport.pdf" "ex-rapport" 1715675326.19786 2
"/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc" 1711186958 2900 1537cc8184ad1792082cd229ecc269f4 "" "/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc" 1713199481 2971 def0b6c1f0b107b3b936def894055589 ""
"/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1711186958 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1713199481 3524 cb3e574dea2d1052e39280babc910dc8 ""
"/usr/share/texmf-dist/fonts/tfm/jknappen/ec/tcrm1000.tfm" 1711186958 1536 e07581a4bb3136ece9eeb4c3ffab8233 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm" 1713199481 3584 2d666ecf6d466d8b007246bc2f94d9da ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmbx10.tfm" 1711186958 1328 c834bbb027764024c09d3d2bf908b5f0 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecbx1440.tfm" 1713199481 3584 13049b61b922a28b158a38aeff75ee9b ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmbx12.tfm" 1711186958 1324 c910af8c371558dc20f2d7822f66fe64 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm0900.tfm" 1713199481 3584 d3d8ac8b25ca19c0a40b86a5db1e8ccc ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm" 1711186958 1524 4414a8315f39513458b80dfc63bff03a "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm" 1713199481 3584 adb004a0c8e7c46ee66cad73671f37b4 ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm" 1711186958 1512 f21f83efb36853c0b70002322c1ab3ad "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1200.tfm" 1713199481 3584 f80ddd985bd00e29e9a6047ebd9d4781 ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi8.tfm" 1711186958 1520 eccf95517727cb11801f4f1aee3a21b4 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1440.tfm" 1713199481 3584 3169d30142b88a27d4ab0e3468e963a2 ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1711186958 1288 655e228510b4c2a1abe905c368440826 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1728.tfm" 1713199481 3584 3c76ccb63eda935a68ba65ba9da29f1a ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmr17.tfm" 1711186958 1292 296a67155bdbfc32aa9c636f21e91433 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm" 1713199481 3072 3bce340d4c075dffe6d4ec732b4c32fe ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmr6.tfm" 1711186958 1300 b62933e007d01cfd073f79b963c01526 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ectt0900.tfm" 1713199481 1536 ae7aab2f8a4bc9edfce2899f53ba88c3 ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmr8.tfm" 1711186958 1292 21c1c5bfeaebccffdb478fd231a0997d "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm" 1713199481 1536 06717a2b50de47d4087ac0e6cd759455 ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1711186958 1124 6c73e740cf17375f03eec0ee63599741 "" "/usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1713199481 1004 54797486969f23fa377b128694d548df ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1711186958 1116 933a60c408fc0a863a92debe84b2d294 "" "/usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex8.tfm" 1713199481 988 bdf658c3bfc2d96d3c8b02cfc1c94c20 ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1711186958 1120 8b7d695260f3cff42e636090a8002094 "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmex10.tfm" 1713199481 992 662f679a0b3d2d53c1b94050fdaa3f50 ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmti10.tfm" 1711186958 1480 aa8e34af0eb6a2941b776984cf1dfdc4 "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm" 1713199481 1524 4414a8315f39513458b80dfc63bff03a ""
"/usr/share/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm" 1711186958 768 1321e9409b4137d6fb428ac9dc956269 "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm" 1713199481 1512 f21f83efb36853c0b70002322c1ab3ad ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb" 1711186958 34811 78b52f49e893bcba91bd7581cdc144c0 "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi8.tfm" 1713199481 1520 eccf95517727cb11801f4f1aee3a21b4 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb" 1711186958 32080 340ef9bf63678554ee606688e7b5339d "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1713199481 1288 655e228510b4c2a1abe905c368440826 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb" 1711186958 30251 6afa5cb1d0204815a708a080681d4674 "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr6.tfm" 1713199481 1300 b62933e007d01cfd073f79b963c01526 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1711186958 36299 5f9df58c2139e7edcf37c8fca4bd384d "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr8.tfm" 1713199481 1292 21c1c5bfeaebccffdb478fd231a0997d ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb" 1711186958 36281 c355509802a035cadc5f15869451dcee "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1713199481 1124 6c73e740cf17375f03eec0ee63599741 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1711186958 35752 024fb6c41858982481f6968b5fc26508 "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1713199481 1116 933a60c408fc0a863a92debe84b2d294 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb" 1711186958 32722 d7379af29a190c3f453aba36302ff5a9 "" "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1713199481 1120 8b7d695260f3cff42e636090a8002094 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb" 1711186958 32362 179c33bbf43f19adbb3825bb4e36e57a "" "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1713199481 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb" 1711186958 32762 224316ccc9ad3ca0423a14971cfa7fc1 "" "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb" 1713199481 36741 fa121aac0049305630cf160b86157ee4 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1711186958 32569 5e5ddc8df908dea60932f3c484a54c0d "" "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1713199481 35752 024fb6c41858982481f6968b5fc26508 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb" 1711186958 32716 08e384dc442464e7285e891af9f45947 "" "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1713199481 32569 5e5ddc8df908dea60932f3c484a54c0d ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb" 1711186958 37944 359e864bd06cde3b1cf57bb20757fb06 "" "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb" 1713199481 145408 43d44302ca7d82d487f511f83e309505 ""
"/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb" 1711186958 31099 c85edf1dd5b9e826d67c9c7293b6786c "" "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb" 1713199481 135942 859a90cad7494a1e79c94baf546d7de5 ""
"/usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb" 1711186958 138258 6525c253f16cededa14c7fd0da7f67b2 "" "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb" 1713199481 138258 6525c253f16cededa14c7fd0da7f67b2 ""
"/usr/share/texmf-dist/tex/latex/base/article.cls" 1711186958 20144 147463a6a579f4597269ef9565205cfe "" "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb" 1713199481 136101 f533469f523533d38317ab5729d00c8a ""
"/usr/share/texmf-dist/tex/latex/base/inputenc.sty" 1711186958 5048 425739d70251273bf93e3d51f3c40048 "" "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb" 1713199481 131438 3aa300b3e40e5c8ba7b4e5c6cebc5dd6 ""
"/usr/share/texmf-dist/tex/latex/base/size10.clo" 1711186958 8448 dbc0dbf4156c0bb9ba01a1c685d3bad0 "" "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb" 1713199481 186554 e8f0fa8ca05e038f257a06405232745f ""
"/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1711186958 30006 3d512c0edd558928ddea1690180ef77e "" "/usr/share/texmf-dist/fonts/type1/public/cm-super/sftt0900.pfb" 1713199481 170827 2e4b634de7b58578eae1dc93e51dfe48 ""
"/usr/share/texmf-dist/web2c/texmf.cnf" 1711186958 41588 b43d3e860a4f94167ee1e725ff526a72 "" "/usr/share/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb" 1713199481 169201 9ebf99020dde51a5086e186761a34e8f ""
"/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1711285693.39514 5312047 b07fcd2a9090df96fc745b92a3db793b "" "/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii" 1713199481 71627 94eb9990bed73c364d7f53f960cc8c5b ""
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1711285673 7112991 931bea6825d58058da953e5791f38d28 "" "/usr/share/texmf-dist/tex/generic/babel-french/french.ldf" 1713199481 67734 26e5b5a8646364e31f616588e683938d ""
"ex-rapport.aux" 1715617081.51618 467 dfd15de10c0a5a19b1ec96e1b8771110 "pdflatex" "/usr/share/texmf-dist/tex/generic/babel/babel.sty" 1713199481 146276 10a40dabec03ce18494af0c3a51bcbdc ""
"ex-rapport.bbl" 1715617052.46499 278 e38e720b0bd39c2772a1f07ef75f9a82 "bibtex ex-rapport" "/usr/share/texmf-dist/tex/generic/babel/locale/fr/babel-fr.ini" 1713199481 5918 0f6ad8bc9a16ae22ee21685f58ff516d ""
"ex-rapport.tex" 1715617079.95278 2559 ef60cfa68621adc180317e6d98483611 "" "/usr/share/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex" 1713199481 2133 44b1afb9708604e2ff17e4a838a966b6 ""
"/usr/share/texmf-dist/tex/generic/babel/txtbabel.def" 1713199481 6948 df63e25be1d2bc35bbad5a0141f41348 ""
"/usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty" 1713199481 2222 499d61426192c39efd8f410ee1a52b9c ""
"/usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty" 1713199481 4173 82ac04dfb1256038fad068287fbb4fe6 ""
"/usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty" 1713199481 88371 d84032c0f422c3d1e282266c01bef237 ""
"/usr/share/texmf-dist/tex/latex/amsmath/amsopn.sty" 1713199481 4474 b811654f4bf125f11506d13d13647efb ""
"/usr/share/texmf-dist/tex/latex/amsmath/amstext.sty" 1713199481 2444 0d0c1ee65478277e8015d65b86983da2 ""
"/usr/share/texmf-dist/tex/latex/base/article.cls" 1713199481 20144 147463a6a579f4597269ef9565205cfe ""
"/usr/share/texmf-dist/tex/latex/base/fontenc.sty" 1713199481 5119 a04a8b68ab4f6ce800a41f7f8012a10e ""
"/usr/share/texmf-dist/tex/latex/base/size10.clo" 1713199481 8448 dbc0dbf4156c0bb9ba01a1c685d3bad0 ""
"/usr/share/texmf-dist/tex/latex/base/t1cmtt.fd" 1713199481 2443 790016d75def8d3127df5c216a45abcc ""
"/usr/share/texmf-dist/tex/latex/carlisle/scalefnt.sty" 1713199481 1360 df2086bf924b14b72d6121fe9502fcdb ""
"/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg" 1713199481 1213 620bba36b25224fa9b7e1ccb4ecb76fd ""
"/usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def" 1713199481 19448 1e988b341dda20961a6b931bcde55519 ""
"/usr/share/texmf-dist/tex/latex/graphics/keyval.sty" 1713199481 2671 7e67d78d9b88c845599a85b2d41f2e39 ""
"/usr/share/texmf-dist/tex/latex/graphics/mathcolor.ltx" 1713199481 2885 9c645d672ae17285bba324998918efd8 ""
"/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1713199481 30006 3d512c0edd558928ddea1690180ef77e ""
"/usr/share/texmf-dist/tex/latex/listings/listings.cfg" 1713199481 1830 20af84c556326f7c12b9202ebe363f56 ""
"/usr/share/texmf-dist/tex/latex/listings/listings.sty" 1713199481 81322 d02238bdeb305f2c9f9d0229f99371d0 ""
"/usr/share/texmf-dist/tex/latex/listings/lstlang1.sty" 1713199481 205167 fca232873050cd2da4f9c0c32402c38a ""
"/usr/share/texmf-dist/tex/latex/listings/lstlang2.sty" 1713199481 93888 276ea2c46a9802155d8e1165b7aaad8e ""
"/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty" 1713199481 77022 5c8c440739265e7ba15b8379ece6ecd7 ""
"/usr/share/texmf-dist/tex/latex/listings/lstpatch.sty" 1713199481 329 f19f5da7234b51d16764e23d20999c73 ""
"/usr/share/texmf-dist/tex/latex/mdwtools/syntax.sty" 1713199481 19268 1cc67e61681d15dc7bfddab7602a9cd1 ""
"/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty" 1713199481 55487 80a65caedd3722f4c20a14a69e785d8f ""
"/usr/share/texmf-dist/web2c/texmf.cnf" 1713199481 41588 b43d3e860a4f94167ee1e725ff526a72 ""
"/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1715669800.4283 5312086 49e033e8d3948bcca48e0612d8828e70 ""
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1715669744 7119913 84688908edcaa506b571016b2546b806 ""
"ex-rapport.aux" 1715675325.91528 1056 73909169f0984220be1f002f5c1fdca4 "pdflatex"
"ex-rapport.bbl" 1715673124.50549 167 f13b79c5d213ac0741acd90cb6ff3d89 "bibtex ex-rapport"
"ex-rapport.tex" 1715675323.56847 4800 822b40565accad567b431e11f1652783 ""
(generated) (generated)
"ex-rapport.aux" "ex-rapport.aux"
"ex-rapport.log" "ex-rapport.log"

113
RapportPresentation/ex-rapport.fls
View File

@ -8,16 +8,78 @@ INPUT /usr/share/texmf-dist/tex/latex/base/article.cls
INPUT /usr/share/texmf-dist/tex/latex/base/size10.clo INPUT /usr/share/texmf-dist/tex/latex/base/size10.clo
INPUT /usr/share/texmf-dist/tex/latex/base/size10.clo INPUT /usr/share/texmf-dist/tex/latex/base/size10.clo
INPUT /usr/share/texmf-dist/tex/latex/base/size10.clo INPUT /usr/share/texmf-dist/tex/latex/base/size10.clo
INPUT /usr/share/texmf-dist/tex/latex/base/inputenc.sty INPUT /usr/share/texmf-dist/tex/latex/base/fontenc.sty
INPUT /usr/share/texmf-dist/tex/latex/base/inputenc.sty INPUT /usr/share/texmf-dist/tex/latex/base/fontenc.sty
INPUT /usr/share/texmf-dist/fonts/map/fontname/texfonts.map
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm
INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty
INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty
INPUT /usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg
INPUT /usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg
INPUT /usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg
INPUT /usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def
INPUT /usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def
INPUT /usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def
INPUT /usr/share/texmf-dist/tex/latex/graphics/mathcolor.ltx
INPUT /usr/share/texmf-dist/tex/latex/graphics/mathcolor.ltx
INPUT /usr/share/texmf-dist/tex/latex/graphics/mathcolor.ltx
INPUT /usr/share/texmf-dist/tex/generic/babel/babel.sty
INPUT /usr/share/texmf-dist/tex/generic/babel/babel.sty
INPUT /usr/share/texmf-dist/tex/generic/babel/txtbabel.def
INPUT /usr/share/texmf-dist/tex/generic/babel-french/french.ldf
INPUT /usr/share/texmf-dist/tex/generic/babel-french/french.ldf
INPUT /usr/share/texmf-dist/tex/generic/babel-french/french.ldf
INPUT /usr/share/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex
INPUT /usr/share/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex
INPUT /usr/share/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex
INPUT /usr/share/texmf-dist/tex/generic/babel/locale/fr/babel-fr.ini
INPUT /usr/share/texmf-dist/tex/latex/carlisle/scalefnt.sty
INPUT /usr/share/texmf-dist/tex/latex/carlisle/scalefnt.sty
INPUT /usr/share/texmf-dist/tex/latex/graphics/keyval.sty
INPUT /usr/share/texmf-dist/tex/latex/graphics/keyval.sty
INPUT /usr/share/texmf-dist/tex/latex/mdwtools/syntax.sty
INPUT /usr/share/texmf-dist/tex/latex/mdwtools/syntax.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/listings.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/listings.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstpatch.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstpatch.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstpatch.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/share/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstlang1.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstlang1.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstlang1.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstlang2.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstlang2.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstlang2.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def INPUT /usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
INPUT /usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def INPUT /usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
INPUT ./ex-rapport.aux INPUT ./ex-rapport.aux
INPUT ./ex-rapport.aux INPUT ./ex-rapport.aux
INPUT ex-rapport.aux INPUT ex-rapport.aux
OUTPUT ex-rapport.aux OUTPUT ex-rapport.aux
INPUT /usr/share/texmf-dist/fonts/map/fontname/texfonts.map INPUT /usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr17.tfm INPUT /usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1728.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1200.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr12.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr12.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr8.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr8.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr6.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr6.tfm
@ -27,30 +89,41 @@ INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmex10.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex8.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1440.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecbx1440.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm0900.tfm
INPUT /usr/share/texmf-dist/tex/latex/base/t1cmtt.fd
INPUT /usr/share/texmf-dist/tex/latex/base/t1cmtt.fd
INPUT /usr/share/texmf-dist/tex/latex/base/t1cmtt.fd
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ectt0900.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr12.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr12.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmbx12.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmbx10.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/tcrm1000.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmex10.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm
OUTPUT ex-rapport.pdf OUTPUT ex-rapport.pdf
INPUT /var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map INPUT /var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map
INPUT /usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc INPUT /usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc
INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm
INPUT ./ex-rapport.bbl INPUT ./ex-rapport.bbl
INPUT ./ex-rapport.bbl INPUT ./ex-rapport.bbl
INPUT ex-rapport.bbl INPUT ex-rapport.bbl
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmti10.tfm
INPUT ex-rapport.aux INPUT ex-rapport.aux
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sftt0900.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb

415
RapportPresentation/ex-rapport.log
View File

@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.3.24) 13 MAY 2024 18:18 This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.5.14) 14 MAY 2024 10:28
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
file:line:error style messages enabled. file:line:error style messages enabled.
@ -23,67 +23,390 @@ File: size10.clo 2023/05/17 v1.4n Standard LaTeX file (size option)
\abovecaptionskip=\skip48 \abovecaptionskip=\skip48
\belowcaptionskip=\skip49 \belowcaptionskip=\skip49
\bibindent=\dimen140 \bibindent=\dimen140
) (/usr/share/texmf-dist/tex/latex/base/inputenc.sty ) (/usr/share/texmf-dist/tex/latex/base/fontenc.sty
Package: inputenc 2021/02/14 v1.3d Input encoding file Package: fontenc 2021/04/29 v2.0v Standard LaTeX package
\inpenc@prehook=\toks17 ) (/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty
\inpenc@posthook=\toks18 Package: xcolor 2023/11/15 v3.01 LaTeX color extensions (UK)
(/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg
File: color.cfg 2016/01/02 v1.6 sample color configuration
)
Package xcolor Info: Driver file: pdftex.def on input line 274.
(/usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def
File: pdftex.def 2022/09/22 v1.2b Graphics/color driver for pdftex
) (/usr/share/texmf-dist/tex/latex/graphics/mathcolor.ltx)
Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1350.
Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1354.
Package xcolor Info: Model `RGB' extended on input line 1366.
Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1368.
Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1369.
Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1370.
Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1371.
Package xcolor Info: Model `Gray' substituted by `gray' on input line 1372.
Package xcolor Info: Model `wave' substituted by `hsb' on input line 1373.
) (/usr/share/texmf-dist/tex/generic/babel/babel.sty
Package: babel 2024/02/07 v24.2 The Babel package
\babel@savecnt=\count196
\U@D=\dimen141
\l@unhyphenated=\language7
(/usr/share/texmf-dist/tex/generic/babel/txtbabel.def)
\bbl@readstream=\read2
\bbl@dirlevel=\count197
(/usr/share/texmf-dist/tex/generic/babel-french/french.ldf
Language: french 2024-02-29 v3.5s French support from the babel system
Package babel Info: Hyphen rules for 'acadian' set to \l@french
(babel) (\language6). Reported on input line 91.
Package babel Info: Hyphen rules for 'canadien' set to \l@french
(babel) (\language6). Reported on input line 92.
\FB@stdchar=\count198
Package babel Info: Making : an active character on input line 420.
Package babel Info: Making ; an active character on input line 421.
Package babel Info: Making ! an active character on input line 422.
Package babel Info: Making ? an active character on input line 423.
\FBguill@level=\count199
\FBold@everypar=\toks17
\FB@Mht=\dimen142
\mc@charclass=\count266
\mc@charfam=\count267
\mc@charslot=\count268
\std@mcc=\count269
\dec@mcc=\count270
\FB@parskip=\dimen143
\listindentFB=\dimen144
\descindentFB=\dimen145
\labelindentFB=\dimen146
\labelwidthFB=\dimen147
\leftmarginFB=\dimen148
\parindentFFN=\dimen149
\FBfnindent=\dimen150
)) (/usr/share/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex
Package babel Info: Importing font and identification data for french
(babel) from babel-fr.ini. Reported on input line 11.
) (/usr/share/texmf-dist/tex/latex/carlisle/scalefnt.sty) (/usr/share/texmf-dist/tex/latex/graphics/keyval.sty
Package: keyval 2022/05/29 v1.15 key=value parser (DPC)
\KV@toks@=\toks18
) (/usr/share/texmf-dist/tex/latex/mdwtools/syntax.sty
Package: syntax 1996/05/17 1.07 Syntax typesetting (MDW)
\grammarparsep=\skip50
\grammarindent=\dimen151
\sdstartspace=\skip51
\sdendspace=\skip52
\sdmidskip=\skip53
\sdtokskip=\skip54
\sdfinalskip=\skip55
\sdrulewidth=\dimen152
\sdcirclediam=\dimen153
\sdindent=\dimen154
) (/usr/share/texmf-dist/tex/latex/listings/listings.sty
\lst@mode=\count271
\lst@gtempboxa=\box51
\lst@token=\toks19
\lst@length=\count272
\lst@currlwidth=\dimen155
\lst@column=\count273
\lst@pos=\count274
\lst@lostspace=\dimen156
\lst@width=\dimen157
\lst@newlines=\count275
\lst@lineno=\count276
\lst@maxwidth=\dimen158
(/usr/share/texmf-dist/tex/latex/listings/lstpatch.sty
File: lstpatch.sty 2024/02/21 1.10 (Carsten Heinz)
) (/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
File: lstmisc.sty 2024/02/21 1.10 (Carsten Heinz)
\c@lstnumber=\count277
\lst@skipnumbers=\count278
\lst@framebox=\box52
) (/usr/share/texmf-dist/tex/latex/listings/listings.cfg
File: listings.cfg 2024/02/21 1.10 listings configuration
))
Package: listings 2024/02/21 1.10 (Carsten Heinz)
(/usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty
Package: amsmath 2023/05/13 v2.17o AMS math features
\@mathmargin=\skip56
For additional information on amsmath, use the `?' option.
(/usr/share/texmf-dist/tex/latex/amsmath/amstext.sty
Package: amstext 2021/08/26 v2.01 AMS text
(/usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty
File: amsgen.sty 1999/11/30 v2.0 generic functions
\@emptytoks=\toks20
\ex@=\dimen159
)) (/usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d Bold Symbols
\pmbraise@=\dimen160
) (/usr/share/texmf-dist/tex/latex/amsmath/amsopn.sty
Package: amsopn 2022/04/08 v2.04 operator names
)
\inf@bad=\count279
LaTeX Info: Redefining \frac on input line 234.
\uproot@=\count280
\leftroot@=\count281
LaTeX Info: Redefining \overline on input line 399.
LaTeX Info: Redefining \colon on input line 410.
\classnum@=\count282
\DOTSCASE@=\count283
LaTeX Info: Redefining \ldots on input line 496.
LaTeX Info: Redefining \dots on input line 499.
LaTeX Info: Redefining \cdots on input line 620.
\Mathstrutbox@=\box53
\strutbox@=\box54
LaTeX Info: Redefining \big on input line 722.
LaTeX Info: Redefining \Big on input line 723.
LaTeX Info: Redefining \bigg on input line 724.
LaTeX Info: Redefining \Bigg on input line 725.
\big@size=\dimen161
LaTeX Font Info: Redeclaring font encoding OML on input line 743.
LaTeX Font Info: Redeclaring font encoding OMS on input line 744.
\macc@depth=\count284
LaTeX Info: Redefining \bmod on input line 905.
LaTeX Info: Redefining \pmod on input line 910.
LaTeX Info: Redefining \smash on input line 940.
LaTeX Info: Redefining \relbar on input line 970.
LaTeX Info: Redefining \Relbar on input line 971.
\c@MaxMatrixCols=\count285
\dotsspace@=\muskip16
\c@parentequation=\count286
\dspbrk@lvl=\count287
\tag@help=\toks21
\row@=\count288
\column@=\count289
\maxfields@=\count290
\andhelp@=\toks22
\eqnshift@=\dimen162
\alignsep@=\dimen163
\tagshift@=\dimen164
\tagwidth@=\dimen165
\totwidth@=\dimen166
\lineht@=\dimen167
\@envbody=\toks23
\multlinegap=\skip57
\multlinetaggap=\skip58
\mathdisplay@stack=\toks24
LaTeX Info: Redefining \[ on input line 2953.
LaTeX Info: Redefining \] on input line 2954.
) (/usr/share/texmf-dist/tex/latex/listings/lstlang1.sty
File: lstlang1.sty 2024/02/21 1.10 listings language file
) (/usr/share/texmf-dist/tex/latex/listings/lstlang2.sty
File: lstlang2.sty 2024/02/21 1.10 listings language file
) (/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty
File: lstmisc.sty 2024/02/21 1.10 (Carsten Heinz)
) (/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def ) (/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2024-02-20 L3 backend support: PDF output (pdfTeX) File: l3backend-pdftex.def 2024-02-20 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count196 \l__color_backend_stack_int=\count291
\l__pdf_internal_box=\box51 \l__pdf_internal_box=\box55
) (./ex-rapport.aux) ) (./ex-rapport.aux)
\openout1 = `ex-rapport.aux'. \openout1 = `ex-rapport.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 36. LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 49.
LaTeX Font Info: ... okay on input line 36. LaTeX Font Info: ... okay on input line 49.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 36. LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 49.
LaTeX Font Info: ... okay on input line 36. LaTeX Font Info: ... okay on input line 49.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 36. LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 49.
LaTeX Font Info: ... okay on input line 36. LaTeX Font Info: ... okay on input line 49.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 36. LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 49.
LaTeX Font Info: ... okay on input line 36. LaTeX Font Info: ... okay on input line 49.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 36. LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 49.
LaTeX Font Info: ... okay on input line 36. LaTeX Font Info: ... okay on input line 49.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 36. LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 49.
LaTeX Font Info: ... okay on input line 36. LaTeX Font Info: ... okay on input line 49.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 36. LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 49.
LaTeX Font Info: ... okay on input line 36. LaTeX Font Info: ... okay on input line 49.
LaTeX Font Info: External font `cmex10' loaded for size (/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
(Font) <12> on input line 38. [Loading MPS to PDF converter (version 2006.09.02).]
LaTeX Font Info: External font `cmex10' loaded for size \scratchcounter=\count292
(Font) <8> on input line 38. \scratchdimen=\dimen168
LaTeX Font Info: External font `cmex10' loaded for size \scratchbox=\box56
(Font) <6> on input line 38. \nofMPsegments=\count293
\nofMParguments=\count294
\everyMPshowfont=\toks25
\MPscratchCnt=\count295
\MPscratchDim=\dimen169
\MPnumerator=\count296
\makeMPintoPDFobject=\count297
\everyMPtoPDFconversion=\toks26
)
LaTeX Info: Redefining \degres on input line 49.
LaTeX Info: Redefining \up on input line 49.
\c@lstlisting=\count298
LaTeX Font Info: Trying to load font information for T1+cmtt on input line 70.
(/usr/share/texmf-dist/tex/latex/base/t1cmtt.fd
File: t1cmtt.fd 2023/04/13 v2.5m Standard LaTeX font definitions
) [1
Overfull \hbox (2.56294pt too wide) in paragraph at lines 42--45 {/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc}]
\OT1/cmr/m/n/10 Nous avons pro-gramm^^Se \OT1/cmr/bx/n/10 en D\OT1/cmr/m/n/10 , en in-terfa^^Xcant notre pro-gramme avec des morceaux LaTeX Font Info: Font shape `T1/cmtt/bx/n' in size <9> not available
[] (Font) Font shape `T1/cmtt/m/n' tried instead on input line 129.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <7> on input line 51.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <5> on input line 51.
[1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}] (./ex-rapport.bbl) [2] (./ex-rapport.aux) LaTeX Font Warning: Command \small invalid in math mode on input line 151.
./ex-rapport.tex:151: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.151 {\Gamma \vdash \lstinline{x : A}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
LaTeX Font Warning: Command \small invalid in math mode on input line 151.
./ex-rapport.tex:151: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.151 {\Gamma \vdash \lstinline{x : A}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
LaTeX Font Warning: Command \small invalid in math mode on input line 157.
./ex-rapport.tex:157: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.157 ...sh \lstinline{fun (x : A) => M : A -> B}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
LaTeX Font Warning: Command \small invalid in math mode on input line 157.
./ex-rapport.tex:157: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.157 ...sh \lstinline{fun (x : A) => M : A -> B}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
./ex-rapport.tex:157: LaTeX Error: Command \bfseries invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.157 ...sh \lstinline{fun (x : A) => M : A -> B}}
Please use the math alphabet \mathbf instead of the \bfseries command.
LaTeX Font Warning: Command \small invalid in math mode on input line 163.
./ex-rapport.tex:163: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.163 ...a \vdash \lstinline{M N} : \lstinline{B}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
LaTeX Font Warning: Command \small invalid in math mode on input line 163.
./ex-rapport.tex:163: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.163 ...a \vdash \lstinline{M N} : \lstinline{B}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
LaTeX Font Warning: Command \small invalid in math mode on input line 163.
./ex-rapport.tex:163: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.163 ...a \vdash \lstinline{M N} : \lstinline{B}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
LaTeX Font Warning: Command \small invalid in math mode on input line 163.
./ex-rapport.tex:163: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.163 ...a \vdash \lstinline{M N} : \lstinline{B}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
LaTeX Font Warning: Command \small invalid in math mode on input line 169.
./ex-rapport.tex:169: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.169 {\Gamma \vdash \lstinline{exf (M : A) : A}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
LaTeX Font Warning: Command \small invalid in math mode on input line 169.
./ex-rapport.tex:169: LaTeX Error: Command \ttfamily invalid in math mode.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.169 {\Gamma \vdash \lstinline{exf (M : A) : A}}
Please use the math alphabet \mathtt instead of the \ttfamilyFB command.
(./ex-rapport.bbl [2]) [3] (./ex-rapport.aux)
*********** ***********
LaTeX2e <2023-11-01> patch level 1 LaTeX2e <2023-11-01> patch level 1
L3 programming layer <2024-02-20> L3 programming layer <2024-02-20>
*********** ***********
) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
520 strings out of 476076 6176 strings out of 476047
9772 string characters out of 5793775 90478 string characters out of 5792626
1932187 words of memory out of 5000000 1979187 words of memory out of 5000000
22687 multiletter control sequences out of 15000+600000 28259 multiletter control sequences out of 15000+600000
562866 words of font info for 52 fonts, out of 8000000 for 9000 569761 words of font info for 64 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191 14 hyphenation exceptions out of 8191
35i,6n,50p,213b,197s stack positions out of 10000i,1000n,20000p,200000b,200000s 56i,8n,65p,214b,1232s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb> </usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sftt0900.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb>
Output written on ex-rapport.pdf (2 pages, 146670 bytes). Output written on ex-rapport.pdf (3 pages, 185810 bytes).
PDF statistics: PDF statistics:
82 PDF objects out of 1000 (max. 8388607) 75 PDF objects out of 1000 (max. 8388607)
49 compressed objects within 1 object stream 45 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000) 0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000) 1 words of extra memory for PDF output out of 10000 (max. 10000000)

BIN
RapportPresentation/ex-rapport.pdf
View File

Binary file not shown.

BIN
RapportPresentation/ex-rapport.synctex.gz
View File

Binary file not shown.

157
RapportPresentation/ex-rapport.tex
View File

@ -1,7 +1,21 @@
\documentclass{article} \documentclass{article}
\usepackage[utf8]{inputenc} \usepackage[T1]{fontenc}
%%\usepackage[francais]{babel} installer texlive-lang-french pour cela \usepackage{xcolor}
\usepackage[french]{babel}
\usepackage{syntax}
\usepackage{listings}
\usepackage{amsmath}
\lstset{
language=caml,
columns=[c]fixed,
basicstyle=\small\ttfamily,
keywordstyle=\bfseries,
upquote=true,
commentstyle=,
breaklines=true,
showstringspaces=false}
%% installer texlive-lang-french pour cela
% ci-dessous: commenté car non offert sur les machines libre-service. % ci-dessous: commenté car non offert sur les machines libre-service.
% décommentez si vous le souhaitez. % décommentez si vous le souhaitez.
@ -28,74 +42,141 @@
\author{Marwan et Augustin} \author{Marwan et Augustin}
\date{} \date{}
% definition de quelques macros, pour les maths % definition de quelques macros, pour les maths
\newcommand{\litt}{\alpha} \newcommand{\litt}{\alpha}
\newcommand{\non}[1]{\overline{#1}} \newcommand{\non}[1]{\overline{#1}}
\newcommand{\TODO}[1]{\textbf{\color{red}#1}}
\begin{document} \begin{document}
\maketitle \maketitle
\section{Présentation} \section{Présentation}
Nous avons programmé \textbf{en D}, en interfaçant notre programme Nous avons programmé \textbf{Pieuvre}, un assistant de preuve
avec des morceaux d'assembleur que nous avons écrits à la main, entre pour la logique intuitionniste en \textbf{OCaml}.
3 et 4 heures du matin uniquement sinon ça ne compte pas. Il permet, à l'aide d'une boucle interactive, de prouver des
prédicats simples.
Nous indiquons dans la partie~\ref{s:opt} comment compiler,
lancer et utiliser notre programme.
Nous exposons ensuite à la partie~\ref{s:orga} comment notre
programme est structuré.
Nous présentons enfin dans~\ref{s:stlc} notre implémentation
du $\lambda$-calcul simplement typé puis \ref{s:proof}
notre implémentation des preuves.
\section{Compiler et exécuter}
\label{s:opt}
Pour compiler : \lstinline{make pieuvre}
Nous exposons à la partie~\ref{s:orga} comment notre programme est structuré. Pour exécuter \textbf{Pieuvre} et entrer dans la boucle
interactive de l'assistant de preuve, il suffit d'entrer la
commande \lstinline{./pieuvre}.
Sinon, on peut spécifier un des modes suivants:
\begin{itemize}
\item \texttt{-alpha}
qui vérifie l'$\alpha$-équivalence
de deux $\lambda$-termes séparés par \lstinline{&}.
Un peu de maths en \LaTeX: voici un exemple de formule~: \item \texttt{-reduce}
$$
\sum_{i\geq 0} \litt_1\lor\non{\litt_2}\lor\litt_4
$$
On remarque au passage que $\non{\non{\litt}}$ est pareil que $\litt$.
qui affiche les $\beta$-réduction
successives du $\lambda$-terme.
\end{itemize}
\section{Organisation du code} \section{Organisation du code}
\label{s:orga} \label{s:orga}
Le code est structuré de la manière suivante~: Le code est structuré de la manière suivante~:
\begin{itemize} \begin{itemize}
\item bli \item \lstinline{parser.mly} et \lstinline{lexel.mll}
\item bla qui définissent l'analyse
\item blo syntaxique du $\lambda$-calcul simplément typé
\item Digression à propos des Mustélidés. ainsi que des tactiques.
\item \lstinline{lam.ml} qui contient notre implémentation
du $\lambda$-calcul simplement typé.
\item \lstinline{types.ml} qui contient la définition
des \lstinline{types} et \lstinline{typing.ml}
qui implémente l'algorithme de typage bidirectionnel
défini dans la partie~\ref{s:stlc}.
\item \lstinline{proof.ml} qui définit la structure d'une preuve
et implémente les tactiques.
\item \lstinline{main.ml} le point d'entrée de notre programme
qui fait l'interface avec l'utilisateur.
\end{itemize} \end{itemize}
\section{Critique des performances} \section{$\lambda$-calcul simplement typé}
\label{s:stlc}
On constate que blibla. Avant de pouvoir réaliser des preuves, il faut pouvoir les encoder.
On utilise le $\lambda$-calcul simplement typé.
Dans notre programme, on utilise la syntaxe suivante
pour les types et pour les termes:
On est par ailleurs capable de citer des références, ainsi~: \cite{ProjInt16}. \begin{grammar}
<A, B> ::= \lstinline{X}
\alt \lstinline{A -> B}
\alt \lstinline{A /\ B}
\alt \lstinline{A \/ B}
\alt \lstinline{false}
\end{grammar}
\medskip \begin{grammar}
<M, N> ::= x
\alt \lstinline{fun (x : A) => M}
\alt \lstinline{M N}
\alt \lstinline{exf (M : A)}
\end{grammar}
Les termes ainsi définis se réduisent à l'aide des règles de
$\beta$-réduction rappelées dans les notes de
Selinger~\cite{SelingerNotes}.
Avant d'être $\beta$-réduit par \lstinline{betastep},
les termes sont d'abord
$\alpha$-convertis avec \lstinline{alpha_convert} afin d'éviter
les problèmes de substitution.
Pour citer une référence bibliographique, il faut insérer les On remarque que l'on impose d'annoter le type de l'argument
informations correspondantes au format BibTeX dans le fichier d'une $\lambda$-abstraction. Tous les termes sont alors
\texttt{ex-biblio.bib}, et puis faire la citation en utilisant la typables avec les règles bidirectionnelles suivantes:
commande \verb+\cite{tititoto}+.
Ensuite, on compile de la manière suivante~:
\begin{enumerate}
\item \texttt{pdflatex ex-rapport}
et là il proteste, car il a vu une citation de \texttt{tititoto}, mais \TODO{règles de typage}
ne sait pas à quoi cela fait référence
\item \texttt{bibtex ex-rapport} \[
\dfrac
{\lstinline{x : A} \in \Gamma}
{\Gamma \vdash \lstinline{x : A}}
\]
et là il met ensemble les informations pour savoir engendrer \[
l'information correspondant à la citation de \texttt{tititoto} \dfrac
{\Gamma \vdash \lstinline{M : B}}
{\Gamma \vdash \lstinline{fun (x : A) => M : A -> B}}
\]
\item \texttt{pdflatex ex-rapport} \[
\dfrac{\Gamma \vdash M : \lstinline{A -> B}
\quad \Gamma \vdash N : \lstinline{A}}
{\Gamma \vdash \lstinline{M N} : \lstinline{B}}
\]
et là il peut engendrer le fichier pdf, avec la bonne citation et la \[
bonne description dans les références \dfrac
\end{enumerate} {\Gamma \vdash \lstinline{M : false}}
{\Gamma \vdash \lstinline{exf (M : A) : A}}
\]
\section{Preuves}
\label{s:proof}
\TODO{Augustin}
\section{Vérification des preuves}
\TODO{parler de la vérification de preuve,
quelles difficultés ? quelles certitudes ?}
\bibliographystyle{plain} \bibliographystyle{plain}