diff --git a/RapportPresentation/ex-biblio.bib b/RapportPresentation/ex-biblio.bib index 636f9c8..24c1406 100644 --- a/RapportPresentation/ex-biblio.bib +++ b/RapportPresentation/ex-biblio.bib @@ -16,3 +16,14 @@ 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} +} diff --git a/RapportPresentation/ex-rapport.aux b/RapportPresentation/ex-rapport.aux index dbdbe24..80a291e 100644 --- a/RapportPresentation/ex-rapport.aux +++ b/RapportPresentation/ex-rapport.aux @@ -1,10 +1,23 @@ \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 {2}Organisation du code}{1}{}\protected@file@percent } -\newlabel{s:orga}{{2}{1}{}{}{}} -\@writefile{toc}{\contentsline {section}{\numberline {3}Critique des performances}{1}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {2}Compiler et exécuter}{1}{}\protected@file@percent } +\newlabel{s:opt}{{2}{1}{}{}{}} +\@writefile{toc}{\contentsline {section}{\numberline {3}Organisation du code}{1}{}\protected@file@percent } +\newlabel{s:orga}{{3}{1}{}{}{}} +\citation{SelingerNotes} \bibstyle{plain} \bibdata{ex-biblio} -\bibcite{ProjInt16}{1} -\gdef \@abspage@last{2} +\bibcite{SelingerNotes}{1} +\@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} diff --git a/RapportPresentation/ex-rapport.bbl b/RapportPresentation/ex-rapport.bbl index b2bff6d..68ee517 100644 --- a/RapportPresentation/ex-rapport.bbl +++ b/RapportPresentation/ex-rapport.bbl @@ -1,8 +1,8 @@ \begin{thebibliography}{1} -\bibitem{ProjInt16} -Les~M1 du~DI. -\newblock Notre beau projet intégré. -\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. +\bibitem{SelingerNotes} +Peter Selinger. +\newblock Lecture notes on the lambda calculus. +\newblock {\em CoRR}, 2008. \end{thebibliography} diff --git a/RapportPresentation/ex-rapport.blg b/RapportPresentation/ex-rapport.blg index 6201c24..b404b6e 100644 --- a/RapportPresentation/ex-rapport.blg +++ b/RapportPresentation/ex-rapport.blg @@ -5,42 +5,42 @@ The style file: plain.bst Database file #1: ex-biblio.bib You've used 1 entry, 2118 wiz_defined-function locations, - 509 strings with 4174 characters, -and the built_in function-call counts, 453 in all, are: -= -- 45 -> -- 11 -< -- 2 -+ -- 4 -- -- 3 -* -- 31 -:= -- 72 -add.period$ -- 4 + 503 strings with 4086 characters, +and the built_in function-call counts, 224 in all, are: += -- 20 +> -- 7 +< -- 0 ++ -- 3 +- -- 2 +* -- 10 +:= -- 48 +add.period$ -- 3 call.type$ -- 1 change.case$ -- 4 chr.to.int$ -- 0 cite$ -- 1 -duplicate$ -- 22 -empty$ -- 41 -format.name$ -- 3 -if$ -- 101 +duplicate$ -- 10 +empty$ -- 18 +format.name$ -- 2 +if$ -- 42 int.to.chr$ -- 0 int.to.str$ -- 1 missing$ -- 1 newline$ -- 8 -num.names$ -- 4 -pop$ -- 5 +num.names$ -- 2 +pop$ -- 4 preamble$ -- 1 purify$ -- 3 quote$ -- 0 -skip$ -- 16 +skip$ -- 7 stack$ -- 0 -substring$ -- 29 -swap$ -- 11 -text.length$ -- 2 +substring$ -- 5 +swap$ -- 1 +text.length$ -- 0 text.prefix$ -- 0 top$ -- 0 type$ -- 4 warning$ -- 0 -while$ -- 6 +while$ -- 2 width$ -- 2 -write$ -- 15 +write$ -- 12 diff --git a/RapportPresentation/ex-rapport.fdb_latexmk b/RapportPresentation/ex-rapport.fdb_latexmk index b52ed3a..0aa3b92 100644 --- a/RapportPresentation/ex-rapport.fdb_latexmk +++ b/RapportPresentation/ex-rapport.fdb_latexmk @@ -1,54 +1,84 @@ # Fdb version 4 -["bibtex ex-rapport"] 1715617052.40433 "ex-rapport.aux" "ex-rapport.bbl" "ex-rapport" 1715617081.68301 0 - "./ex-biblio.bib" 1493037286 435 eb384d654794ae20bc01965f6b4e4822 "" - "/usr/share/texmf-dist/bibtex/bst/base/plain.bst" 1711186958 20613 bd3fbfa9f64872b81ac57a0dd2ed855f "" - "ex-rapport.aux" 1715617081.51618 467 dfd15de10c0a5a19b1ec96e1b8771110 "pdflatex" +["bibtex ex-rapport"] 1715673124.42722 "ex-rapport.aux" "ex-rapport.bbl" "ex-rapport" 1715675326.19747 0 + "./ex-biblio.bib" 1715672341.14715 878 b24a3ee5eaad1f378a00844cfb93a00b "" + "/usr/share/texmf-dist/bibtex/bst/base/plain.bst" 1713199481 20613 bd3fbfa9f64872b81ac57a0dd2ed855f "" + "ex-rapport.aux" 1715675325.91528 1056 73909169f0984220be1f002f5c1fdca4 "pdflatex" (generated) "ex-rapport.bbl" "ex-rapport.blg" (rewritten before read) -["pdflatex"] 1715617081.286 "ex-rapport.tex" "ex-rapport.pdf" "ex-rapport" 1715617081.6834 0 - "/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc" 1711186958 2900 1537cc8184ad1792082cd229ecc269f4 "" - "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1711186958 3524 cb3e574dea2d1052e39280babc910dc8 "" - "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/tcrm1000.tfm" 1711186958 1536 e07581a4bb3136ece9eeb4c3ffab8233 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmbx10.tfm" 1711186958 1328 c834bbb027764024c09d3d2bf908b5f0 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmbx12.tfm" 1711186958 1324 c910af8c371558dc20f2d7822f66fe64 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm" 1711186958 1524 4414a8315f39513458b80dfc63bff03a "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm" 1711186958 1512 f21f83efb36853c0b70002322c1ab3ad "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi8.tfm" 1711186958 1520 eccf95517727cb11801f4f1aee3a21b4 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1711186958 1288 655e228510b4c2a1abe905c368440826 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr17.tfm" 1711186958 1292 296a67155bdbfc32aa9c636f21e91433 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr6.tfm" 1711186958 1300 b62933e007d01cfd073f79b963c01526 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr8.tfm" 1711186958 1292 21c1c5bfeaebccffdb478fd231a0997d "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1711186958 1124 6c73e740cf17375f03eec0ee63599741 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1711186958 1116 933a60c408fc0a863a92debe84b2d294 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1711186958 1120 8b7d695260f3cff42e636090a8002094 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmti10.tfm" 1711186958 1480 aa8e34af0eb6a2941b776984cf1dfdc4 "" - "/usr/share/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm" 1711186958 768 1321e9409b4137d6fb428ac9dc956269 "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb" 1711186958 34811 78b52f49e893bcba91bd7581cdc144c0 "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb" 1711186958 32080 340ef9bf63678554ee606688e7b5339d "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb" 1711186958 30251 6afa5cb1d0204815a708a080681d4674 "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1711186958 36299 5f9df58c2139e7edcf37c8fca4bd384d "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb" 1711186958 36281 c355509802a035cadc5f15869451dcee "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1711186958 35752 024fb6c41858982481f6968b5fc26508 "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb" 1711186958 32722 d7379af29a190c3f453aba36302ff5a9 "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb" 1711186958 32362 179c33bbf43f19adbb3825bb4e36e57a "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb" 1711186958 32762 224316ccc9ad3ca0423a14971cfa7fc1 "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1711186958 32569 5e5ddc8df908dea60932f3c484a54c0d "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb" 1711186958 32716 08e384dc442464e7285e891af9f45947 "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb" 1711186958 37944 359e864bd06cde3b1cf57bb20757fb06 "" - "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb" 1711186958 31099 c85edf1dd5b9e826d67c9c7293b6786c "" - "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb" 1711186958 138258 6525c253f16cededa14c7fd0da7f67b2 "" - "/usr/share/texmf-dist/tex/latex/base/article.cls" 1711186958 20144 147463a6a579f4597269ef9565205cfe "" - "/usr/share/texmf-dist/tex/latex/base/inputenc.sty" 1711186958 5048 425739d70251273bf93e3d51f3c40048 "" - "/usr/share/texmf-dist/tex/latex/base/size10.clo" 1711186958 8448 dbc0dbf4156c0bb9ba01a1c685d3bad0 "" - "/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1711186958 30006 3d512c0edd558928ddea1690180ef77e "" - "/usr/share/texmf-dist/web2c/texmf.cnf" 1711186958 41588 b43d3e860a4f94167ee1e725ff526a72 "" - "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1711285693.39514 5312047 b07fcd2a9090df96fc745b92a3db793b "" - "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1711285673 7112991 931bea6825d58058da953e5791f38d28 "" - "ex-rapport.aux" 1715617081.51618 467 dfd15de10c0a5a19b1ec96e1b8771110 "pdflatex" - "ex-rapport.bbl" 1715617052.46499 278 e38e720b0bd39c2772a1f07ef75f9a82 "bibtex ex-rapport" - "ex-rapport.tex" 1715617079.95278 2559 ef60cfa68621adc180317e6d98483611 "" +["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-t1.enc" 1713199481 2971 def0b6c1f0b107b3b936def894055589 "" + "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1713199481 3524 cb3e574dea2d1052e39280babc910dc8 "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm" 1713199481 3584 2d666ecf6d466d8b007246bc2f94d9da "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecbx1440.tfm" 1713199481 3584 13049b61b922a28b158a38aeff75ee9b "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm0900.tfm" 1713199481 3584 d3d8ac8b25ca19c0a40b86a5db1e8ccc "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm" 1713199481 3584 adb004a0c8e7c46ee66cad73671f37b4 "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1200.tfm" 1713199481 3584 f80ddd985bd00e29e9a6047ebd9d4781 "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1440.tfm" 1713199481 3584 3169d30142b88a27d4ab0e3468e963a2 "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1728.tfm" 1713199481 3584 3c76ccb63eda935a68ba65ba9da29f1a "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm" 1713199481 3072 3bce340d4c075dffe6d4ec732b4c32fe "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ectt0900.tfm" 1713199481 1536 ae7aab2f8a4bc9edfce2899f53ba88c3 "" + "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm" 1713199481 1536 06717a2b50de47d4087ac0e6cd759455 "" + "/usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1713199481 1004 54797486969f23fa377b128694d548df "" + "/usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex8.tfm" 1713199481 988 bdf658c3bfc2d96d3c8b02cfc1c94c20 "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmex10.tfm" 1713199481 992 662f679a0b3d2d53c1b94050fdaa3f50 "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm" 1713199481 1524 4414a8315f39513458b80dfc63bff03a "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm" 1713199481 1512 f21f83efb36853c0b70002322c1ab3ad "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmmi8.tfm" 1713199481 1520 eccf95517727cb11801f4f1aee3a21b4 "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1713199481 1288 655e228510b4c2a1abe905c368440826 "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr6.tfm" 1713199481 1300 b62933e007d01cfd073f79b963c01526 "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmr8.tfm" 1713199481 1292 21c1c5bfeaebccffdb478fd231a0997d "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1713199481 1124 6c73e740cf17375f03eec0ee63599741 "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1713199481 1116 933a60c408fc0a863a92debe84b2d294 "" + "/usr/share/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1713199481 1120 8b7d695260f3cff42e636090a8002094 "" + "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1713199481 36299 5f9df58c2139e7edcf37c8fca4bd384d "" + "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb" 1713199481 36741 fa121aac0049305630cf160b86157ee4 "" + "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1713199481 35752 024fb6c41858982481f6968b5fc26508 "" + "/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1713199481 32569 5e5ddc8df908dea60932f3c484a54c0d "" + "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb" 1713199481 145408 43d44302ca7d82d487f511f83e309505 "" + "/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" 1713199481 138258 6525c253f16cededa14c7fd0da7f67b2 "" + "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb" 1713199481 136101 f533469f523533d38317ab5729d00c8a "" + "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb" 1713199481 131438 3aa300b3e40e5c8ba7b4e5c6cebc5dd6 "" + "/usr/share/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb" 1713199481 186554 e8f0fa8ca05e038f257a06405232745f "" + "/usr/share/texmf-dist/fonts/type1/public/cm-super/sftt0900.pfb" 1713199481 170827 2e4b634de7b58578eae1dc93e51dfe48 "" + "/usr/share/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb" 1713199481 169201 9ebf99020dde51a5086e186761a34e8f "" + "/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii" 1713199481 71627 94eb9990bed73c364d7f53f960cc8c5b "" + "/usr/share/texmf-dist/tex/generic/babel-french/french.ldf" 1713199481 67734 26e5b5a8646364e31f616588e683938d "" + "/usr/share/texmf-dist/tex/generic/babel/babel.sty" 1713199481 146276 10a40dabec03ce18494af0c3a51bcbdc "" + "/usr/share/texmf-dist/tex/generic/babel/locale/fr/babel-fr.ini" 1713199481 5918 0f6ad8bc9a16ae22ee21685f58ff516d "" + "/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) "ex-rapport.aux" "ex-rapport.log" diff --git a/RapportPresentation/ex-rapport.fls b/RapportPresentation/ex-rapport.fls index 3204819..b88c06f 100644 --- a/RapportPresentation/ex-rapport.fls +++ b/RapportPresentation/ex-rapport.fls @@ -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/inputenc.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/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 ./ex-rapport.aux INPUT ./ex-rapport.aux INPUT ex-rapport.aux OUTPUT ex-rapport.aux -INPUT /usr/share/texmf-dist/fonts/map/fontname/texfonts.map -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/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/cmr8.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/cmsy8.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/cmbx12.tfm -INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmbx10.tfm -INPUT /usr/share/texmf-dist/fonts/tfm/jknappen/ec/tcrm1000.tfm -INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm +INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm +INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm +INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmex10.tfm OUTPUT ex-rapport.pdf 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 /usr/share/texmf-dist/fonts/tfm/public/cm/cmti10.tfm 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/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/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/cmsy7.pfb -INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb -INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb +INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb +INPUT /usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1440.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 diff --git a/RapportPresentation/ex-rapport.log b/RapportPresentation/ex-rapport.log index f0bf395..637ba3e 100644 --- a/RapportPresentation/ex-rapport.log +++ b/RapportPresentation/ex-rapport.log @@ -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 restricted \write18 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 \belowcaptionskip=\skip49 \bibindent=\dimen140 -) (/usr/share/texmf-dist/tex/latex/base/inputenc.sty -Package: inputenc 2021/02/14 v1.3d Input encoding file -\inpenc@prehook=\toks17 -\inpenc@posthook=\toks18 +) (/usr/share/texmf-dist/tex/latex/base/fontenc.sty +Package: fontenc 2021/04/29 v2.0v Standard LaTeX package +) (/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +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 File: l3backend-pdftex.def 2024-02-20 L3 backend support: PDF output (pdfTeX) -\l__color_backend_stack_int=\count196 -\l__pdf_internal_box=\box51 +\l__color_backend_stack_int=\count291 +\l__pdf_internal_box=\box55 ) (./ex-rapport.aux) \openout1 = `ex-rapport.aux'. -LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 36. -LaTeX Font Info: ... okay on input line 36. -LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 36. -LaTeX Font Info: ... okay on input line 36. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 36. -LaTeX Font Info: ... okay on input line 36. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 36. -LaTeX Font Info: ... okay on input line 36. -LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 36. -LaTeX Font Info: ... okay on input line 36. -LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 36. -LaTeX Font Info: ... okay on input line 36. -LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 36. -LaTeX Font Info: ... okay on input line 36. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <12> on input line 38. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <8> on input line 38. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <6> on input line 38. +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 49. +LaTeX Font Info: ... okay on input line 49. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 49. +LaTeX Font Info: ... okay on input line 49. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 49. +LaTeX Font Info: ... okay on input line 49. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 49. +LaTeX Font Info: ... okay on input line 49. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 49. +LaTeX Font Info: ... okay on input line 49. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 49. +LaTeX Font Info: ... okay on input line 49. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 49. +LaTeX Font Info: ... okay on input line 49. + (/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii +[Loading MPS to PDF converter (version 2006.09.02).] +\scratchcounter=\count292 +\scratchdimen=\dimen168 +\scratchbox=\box56 +\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 -\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 - [] +{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc}] +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 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 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 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 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 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 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 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 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 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 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 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 L3 programming layer <2024-02-20> *********** ) Here is how much of TeX's memory you used: - 520 strings out of 476076 - 9772 string characters out of 5793775 - 1932187 words of memory out of 5000000 - 22687 multiletter control sequences out of 15000+600000 - 562866 words of font info for 52 fonts, out of 8000000 for 9000 + 6176 strings out of 476047 + 90478 string characters out of 5792626 + 1979187 words of memory out of 5000000 + 28259 multiletter control sequences out of 15000+600000 + 569761 words of font info for 64 fonts, out of 8000000 for 9000 14 hyphenation exceptions out of 8191 - 35i,6n,50p,213b,197s stack positions out of 10000i,1000n,20000p,200000b,200000s - -Output written on ex-rapport.pdf (2 pages, 146670 bytes). + 56i,8n,65p,214b,1232s stack positions out of 10000i,1000n,20000p,200000b,200000s + +Output written on ex-rapport.pdf (3 pages, 185810 bytes). PDF statistics: - 82 PDF objects out of 1000 (max. 8388607) - 49 compressed objects within 1 object stream + 75 PDF objects out of 1000 (max. 8388607) + 45 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) diff --git a/RapportPresentation/ex-rapport.pdf b/RapportPresentation/ex-rapport.pdf index de30306..c37ea8f 100644 Binary files a/RapportPresentation/ex-rapport.pdf and b/RapportPresentation/ex-rapport.pdf differ diff --git a/RapportPresentation/ex-rapport.synctex.gz b/RapportPresentation/ex-rapport.synctex.gz index 70e0bb2..1876d87 100644 Binary files a/RapportPresentation/ex-rapport.synctex.gz and b/RapportPresentation/ex-rapport.synctex.gz differ diff --git a/RapportPresentation/ex-rapport.tex b/RapportPresentation/ex-rapport.tex index 5dfe9b4..3aac58d 100644 --- a/RapportPresentation/ex-rapport.tex +++ b/RapportPresentation/ex-rapport.tex @@ -1,7 +1,21 @@ \documentclass{article} -\usepackage[utf8]{inputenc} -%%\usepackage[francais]{babel} installer texlive-lang-french pour cela +\usepackage[T1]{fontenc} +\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. % décommentez si vous le souhaitez. @@ -28,74 +42,141 @@ \author{Marwan et Augustin} \date{} - % definition de quelques macros, pour les maths \newcommand{\litt}{\alpha} \newcommand{\non}[1]{\overline{#1}} - +\newcommand{\TODO}[1]{\textbf{\color{red}#1}} \begin{document} \maketitle \section{Présentation} -Nous avons programmé \textbf{en D}, en interfaçant notre programme -avec des morceaux d'assembleur que nous avons écrits à la main, entre -3 et 4 heures du matin uniquement sinon ça ne compte pas. +Nous avons programmé \textbf{Pieuvre}, un assistant de preuve +pour la logique intuitionniste en \textbf{OCaml}. +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~: -$$ -\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$. + \item \texttt{-reduce} + qui affiche les $\beta$-réduction + successives du $\lambda$-terme. +\end{itemize} \section{Organisation du code} \label{s:orga} Le code est structuré de la manière suivante~: \begin{itemize} -\item bli -\item bla -\item blo -\item Digression à propos des Mustélidés. +\item \lstinline{parser.mly} et \lstinline{lexel.mll} + qui définissent l'analyse + syntaxique du $\lambda$-calcul simplément typé + 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} -\section{Critique des performances} - -On constate que blibla. +\section{$\lambda$-calcul simplement typé} +\label{s:stlc} +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} + ::= \lstinline{X} + \alt \lstinline{A -> B} + \alt \lstinline{A /\ B} + \alt \lstinline{A \/ B} + \alt \lstinline{false} +\end{grammar} -\medskip +\begin{grammar} + ::= 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 -informations correspondantes au format BibTeX dans le fichier -\texttt{ex-biblio.bib}, et puis faire la citation en utilisant la -commande \verb+\cite{tititoto}+. +On remarque que l'on impose d'annoter le type de l'argument +d'une $\lambda$-abstraction. Tous les termes sont alors +typables avec les règles bidirectionnelles suivantes: -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 -ne sait pas à quoi cela fait référence +\TODO{règles de typage} -\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 -\end{enumerate} +\[ + \dfrac + {\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}