This commit is contained in:
Julien Marquet 2024-02-04 17:06:16 +01:00
parent cc965423db
commit 060d7f8c77
5 changed files with 80 additions and 8 deletions

12
Main.hs
View file

@ -16,16 +16,18 @@ main = do
route idRoute route idRoute
compile copyFileCompiler compile copyFileCompiler
{-match "index.md" $ do match "index.md" $ do
route $ setExtension "html" route $ setExtension "html"
compile $ pandocCompiler compile $ pandocCompiler
>>= loadAndApplyTemplate "layouts/default.html" defaultContext >>= loadAndApplyTemplate "index.html" defaultContext
>>= relativizeUrls-} >>= relativizeUrls
match "index.html" $ do match "index.html" $ compile templateBodyCompiler
{-match "index.html" $ do
route $ idRoute route $ idRoute
compile $ getResourceBody compile $ getResourceBody
>>= relativizeUrls >>= relativizeUrls-}
match "layouts/*" $ compile templateBodyCompiler match "layouts/*" $ compile templateBodyCompiler

View file

@ -17,7 +17,7 @@ ul {
.pic-small { .pic-small {
float: right; float: right;
width: 80px; width: 100px;
display: none; display: none;
} }
@ -62,7 +62,17 @@ ul {
} }
} }
@media (width > 650px) {
p {
text-indent: 2em;
}
}
.headpar { .headpar {
margin: 18px 0; margin: 18px 0;
} }
.content {
text-align: justify;
}

View file

@ -12,12 +12,19 @@
<a href="#" class="lightbox" id="lightbox"> <a href="#" class="lightbox" id="lightbox">
<span style="background-image: url('/assets/images/pic.jpg')"></span> <span style="background-image: url('/assets/images/pic.jpg')"></span>
</a> </a>
<h2>Sessions Informelles Maths-Info</h2> <h1>Sessions Informelles Maths&#8209;Info</h1>
<div class="headpar"> <div class="headpar">
Organisées à l'École Normale Supérieure - PSL Organisées à l'École Normale Supérieure - PSL
par Julien Marquet-Wagner
et Gabriel Doriath Döhler.
</div> </div>
<div class="headpar"> <div class="headpar">
Notre but est de&nbsp;: Rejoignez notre
<a href="https://chat.whatsapp.com/IU1Y6jtPRoU2fEQExPG7Cx">groupe WhatsApp,</a>
ou demandez-nous en personne&nbsp;!
</div>
<div class="headpar">
Le programme&nbsp;:
<ul> <ul>
<li>Faire des présentations intéressantes</li> <li>Faire des présentations intéressantes</li>
<li>Passer un bon moment <em>et</em> manger</li> <li>Passer un bon moment <em>et</em> manger</li>
@ -28,5 +35,8 @@
d'<a href="https://www.pexels.com/photo/white-tiger-resting-on-rough-land-near-pond-in-zoo-5810713/">ici</a>. d'<a href="https://www.pexels.com/photo/white-tiger-resting-on-rough-land-near-pond-in-zoo-5810713/">ici</a>.
</div> </div>
</div> </div>
<div class="content">
$body$
</div>
</body> </body>
</html> </html>

40
index.md Normal file
View file

@ -0,0 +1,40 @@
## Session 1
- Le jeudi 8/02/2024
- Présentations de 18h30 à 19h30, la suite tant qu'il restera du monde
- Campus Panthéon, la salle n'est pas encore déterminée
#### Présentations
+ Présentation des SIMI
+ Julien Marquet -- Coalgèbres Terminales
+ Gabriel Doriath Döhler -- Présentation de Lean
## SIMI
En SIMI, _Sessions Informelles Maths-Info_, le principe est d'avoir une ou deux
présentations chaque semaine, et d'avoir un repas ensuite.
L'idée vient de nous (Gabriel et Julien). On essaye de faire deux choses en même
temps&nbsp;: d'un côté, on aime bien avoir des projets personnels et on veut se
donner un cadre qui nous motiverait pour les réaliser, et d'un autre, on veut
avoir un endroit qui rejoint le DI et le DMA dans une bonne ambiance.
Penser&nbsp;: le séminaire du DMA et le thé du DMA, par des normalien·ne·s dans
une abiance de club du COF à la HackENS.
Nous avons choisi le thème des types coinductifs et de Lean 4 pour nous donner
un cadre, l'idée étant de ne pas trop nous disperser tout en gardant un champ
de possibilités assez large pour que chacun·e puisse s'amuser.
Du point de vue mathématique, c'est un sujet qui s'étudie avec des outils
catégoriques assez élémentaires.
C'est parfait pour nous&nbsp;: c'est une rare occasion d'entrer dans les
catégories sans avoir à étudier de maths très avancées, et la courbe
d'apprentissage nous est favorable car on peut varier la difficulté entre le
très abordable et le problème ouvert.
Du côté informatique, Lean 4 est à la fois un outil que nous trouvons très
agréable à explorer, et une communauté très active en pleine expansion.
Lean 4 étant à la fois un assistant à la preuve et un langage de programmation,
les thèmes informatiques varient de la pure théorie des types à la compilation.
En d'autres termes, que vous soyez mathématicien·ne ou informaticien·ne,
_il y en a pour tout le monde._

10
layouts/index.html Normal file
View file

@ -0,0 +1,10 @@
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<link rel="stylesheet" type="text/css" href="/assets/css/style.css">
</head>
<body>
$body$
</body>
</html>