diff --git a/content/en/_index.en.md b/content/en/_index.en.md
deleted file mode 100644
index 29f5fb9..0000000
--- a/content/en/_index.en.md
+++ /dev/null
@@ -1,12 +0,0 @@
----
-title: "DéCySif"
-description: "Formal verification in the service of safety and security"
-cascade:
- featured_image: '/images/Decysif.png'
-type: page
----
-
-DéCySif is a regional R&D project funded by an i-Démo call and the
-Ile-de-France French region gathering Adacore, INRIA, OCamlPro and
-TrustInSoft. Its objective is to improve the safety and security of critical
-systems using formal verification tools.
diff --git a/content/en/_index.md b/content/en/_index.md
new file mode 100644
index 0000000..70be460
--- /dev/null
+++ b/content/en/_index.md
@@ -0,0 +1,97 @@
+---
+title: "DéCySif"
+sectiontitle: "Home"
+cascade:
+ featured_image: '/images/Decysif.png'
+description: "Formal verification in the service of safety and security"
+synopsis: "DéCySif is a regional R&D project funded by an i-Démo call and the
+Ile-de-France French region gathering Adacore, INRIA, OCamlPro and TrustInSoft.
+Its objective is to improve the safety and security of critical systems using
+formal verification tools."
+
+project:
+ sectiontitle: "The project"
+ content: "It has been a few years since Rust has proven to be a viable
+ alternative to languages such as Ada/C/C++ in the world of embedded software,
+ critical or not. Current and upcoming actors of the Rust critical embedded
+ software world are now exploring the possibility of using formal analysis
+ tools for Rust.
+
+
+ It is as a direct answer to that question that INRIA have developped Creusot, a
+ tool for Rust. The tool itself is based off the same technological foundations
+ as AdaCore's and TrustInSoft's formal analysis tools: the Why3 platform,
+ developped by INRIA, and a collections of SMT-Solvers such as Alt-Ergo,
+ developped by OCamlPro.
+
+
+ Project DéCySif is the crucible for the improvement of all these tools and
+ aims at guaranteeing convergence towards an optimal solution for the safety
+ and security of embedded systems. "
+
+coordinator:
+ sectiontitle: "Coordinator"
+ content: "TrustInSoft are the coordinators of the project. For any enquiry,
+ please use the [contact form]({{< ref \"contact.en.md\" >}})."
+
+
+collaborators:
+ sectiontitle: "The consortium"
+ consortium:
+ - name: "Adacore"
+ url: "https://www.adacore.com/"
+ description:
+ "Founded in 1994, AdaCore designs and provides software development and
+ verification tools for applications where safety, security, and reliability
+ are critical elements.
+ The use of AdaCore products continues to grow in critical applications such
+ as space systems, commercial avionics, military systems, air traffic
+ control, railway systems, medical devices, or financial services. AdaCore
+ enjoys a substantial and constantly growing base of international clients;
+ visit www.adacore.com/industries/ for more information.
+ AdaCore products are free and come with expert online support provided by
+ the developers themselves. The company has a North American headquarters
+ based in New York and a European headquarters based in Paris."
+
+ - name: "INRIA - LMF - Toccata"
+ url: "https://www.inria.fr/en/toccata"
+ description:
+ "The [INRIA](https://www.inria.fr) is the French national public institute
+ for research in computer science. The INRIA members of the DéCySif project
+ belong to the Formal Methods Laboratory ([LMF](https://lmf.cnrs.fr/))
+ and the Toccata research team
+ ([Toccata](http://toccata.gitlabpages.inria.fr/toccata/)), located in
+ Orsay, France; and jointly affiliated with the University of
+ Paris-Saclay, CNRS, and the INRIA Saclay - Île-de-France research
+ center.
+
+ The general objective of the team is to promote formal specifications
+ and computer-assisted proofs in the development of software requiring a
+ high level of confidence in their safety and adherence to expected
+ behaviors."
+
+ - name: "OCamlPro"
+ url: "https://www.ocamlpro.com"
+ description:
+ "OCamlPro is an R&D consulting firm specializing in engineering problems
+ related to programming languages, business-specific requirements, or
+ technical debt. The company is committed to open source and contributes to
+ the Rust, WebAssembly, and OCaml languages. The company also develops the
+ Alt-Ergo SMT solver used in DéCySif.
+ OCamlPro is also active in the field of Common Criteria certification at
+ the EAL6 level and the use of formal methods (Coq, Lean4, Why3)."
+
+ - name: "TrustInSoft"
+ url: "https://trust-in-soft.com/"
+ description:
+ "TrustInSoft markets tools and services for exhaustive analysis of C and C++
+ source code, providing mathematical guarantees on the quality of their
+ clients' software. These software analysis solutions ensure the security
+ and reliability of source code without altering the development process.
+ These offerings are deployed worldwide among developers and integrators of
+ software components from the aerospace, automotive, railway, military,
+ nuclear, telecoms, or IoT industries."
+
+software:
+ sectiontitle: "Our softwares"
+---
diff --git a/content/en/about.en.md b/content/en/about.en.md
deleted file mode 100644
index bfa8108..0000000
--- a/content/en/about.en.md
+++ /dev/null
@@ -1,39 +0,0 @@
----
-title: "About"
-description: "The Actors of Project DéCySif"
-omit_header_text: true
-featured_image: '/images/Decysif.png'
-type: page
-menu:
- main:
- weight: 2
----
-
-# The project
-
-It has been a few years since Rust has proven to be a viable alternative to
-languages such as Ada/C/C++ in the world of embedded software, critical or not.
-
-Current and upcoming actors of the Rust critical embedded software world are
-now exploring the possibility of using formal analysis tools for Rust.
-
-It is as a direct answer to that question that INRIA have developped Creusot, a
-tool for Rust. The tool itself is based off the same technological foundations
-as AdaCore's and TrustInSoft's formal analysis tools: the Why3 platform,
-developped by INRIA, and a collections of SMT-Solvers such as Alt-Ergo,
-developped by OCamlPro.
-
-Project DéCySif is the crucible for the improvement of all these tools and aims
-at guaranteeing convergence towards an optimal solution for the safety and
-security of embedded systems.
-
-{{< figure src="/images/Organisation-outils.png" >}}
-
-# The consortium
-
-{{< presentation >}}
-
-# Coordinator
-
-TrustInSoft are the coordinators of the project. For any enquiry, please use the [contact form]({{< ref "contact.en.md" >}}).
-
diff --git a/content/fr/_index.fr.md b/content/fr/_index.fr.md
deleted file mode 100644
index 2b4824a..0000000
--- a/content/fr/_index.fr.md
+++ /dev/null
@@ -1,11 +0,0 @@
----
-title: "DéCySif"
-description: "La vérification formelle au service de la sécurité et la sûreté"
-cascade:
- featured_image: '/images/Decysif.png'
-type: page
----
-
-DéCySif est un projet i-Demo régional de R&D regroupant Adacore, l'INRIA,
-OCamlPro et TrustInSoft. Il vise à améliorer la sécurité et la sûreté
-des systèmes critiques en utilisant des outils de vérification formelle.
diff --git a/content/fr/_index.md b/content/fr/_index.md
new file mode 100644
index 0000000..d83ae8d
--- /dev/null
+++ b/content/fr/_index.md
@@ -0,0 +1,98 @@
+---
+title: "DéCySif"
+sectiontitle: "Accueil"
+cascade:
+ featured_image: '/images/Decysif.png'
+description: "La vérification formelle au service de la sécurité et la sûreté"
+synopsis: "DéCySif est un projet i-Demo régional de R&D regroupant Adacore,
+l'INRIA, OCamlPro et TrustInSoft. Il vise à améliorer la sécurité et la sûreté
+des systèmes critiques en utilisant des outils de vérification formelle."
+
+project:
+ sectiontitle: "Le projet"
+ content: "Depuis quelques années, le langage de programmation Rust vient
+ concurrencer les langages Ada/C/C++ établis dans le monde des logiciels
+ critiques, embarqués ou non. Les acteurs actuels et futurs développant des
+ logiciels critiques en Rust se posent désormais la question de l'opportunité
+ d'utiliser des outils d’analyse formelle pour Rust.
+
+
+ C'est pour répondre à cette question que l'outil Creusot pour Rust a été
+ développé par l'INRIA. L'outil est basé sur les mêmes fondations technologiques
+ que les outils d’analyse formelle d’AdaCore et de TrustInSoft : la plateforme
+ Why3 développée par l'INRIA et les mêmes prouveurs automatiques dont le
+ prouveur Alt-Ergo d'OCamlPro.
+
+
+ Le projet DéCySif vie l'amélioration de tous ces outils afin de converger vers
+ une solution optimale pour la sécurité et la sûreté des systèmes critiques."
+
+coordinator:
+ sectiontitle: "Coordinateur"
+ content: "La société TrustInSoft est le coordinateur du projet. Pour toute
+ demande d'information, veuillez passer par le formulaire de [contact]({{< ref \"contact.fr.md\" >}})."
+
+collaborators:
+ sectiontitle: "Le consortium"
+ consortium:
+ - name: "Adacore"
+ url : "https://www.adacore.com/"
+ description:
+ "Fondée en 1994, AdaCore conçoit et fournit des outils de développement et
+ de vérification de logiciels destinés à des applications pour lesquelles la
+ sûreté, la sécurité et la fiabilité sont des éléments critiques.
+ L'utilisation des produits AdaCore connaît une croissance continue dans des
+ applications critiques telles que les systèmes spatiaux, l'avionique
+ commerciale, les systèmes militaires, le contrôle aérien, les systèmes
+ ferroviaires, les appareils médicaux ou les services financiers. AdaCore
+ jouit d'une base fournie de clients internationaux en croissance
+ constante; visitez le site www.adacore.com/industries/ pour de plus amples
+ informations.
+ Les produits AdaCore sont libres et accompagnés d'un support expert en
+ ligne fourni par les développeurs eux-mêmes. La société possède un siège
+ nord-américain basé à New York et un siège européen basé à Paris."
+
+ - name: "INRIA - LMF - Toccata"
+ url: "https://www.inria.fr/fr/toccata"
+ description:
+ "L'[INRIA](https://www.inria.fr) est l'institut national public
+ français de recherche en sciences de l'informatique. Les membres INRIA
+ du projet DéCySif appartiennent au Laboratoire Méthodes Formelles
+ ([LMF](https://lmf.cnrs.fr/)) et à l'équipe de recherche
+ [Toccata](http://toccata.gitlabpages.inria.fr/toccata/), localisés à
+ Orsay, France ; et communs à l'Université Paris-Saclay, au CNRS, et au
+ centre de recherche INRIA Saclay - Île-de-France.
+
+ L'objectif général de l'équipe est de promouvoir les spécifications
+ formelles et les preuves assistées par ordinateur dans le cadre du
+ développement de logiciels requérant un haut niveau de confiance dans
+ leur sûreté de fonctionnement et le respect de comportements attendus."
+
+ - name: "OCamlPro"
+ url: "https://www.ocamlpro.com"
+ description:
+ "OCamlPro est un cabinet d'étude en R&D spécialisé dans les problèmes
+ d'ingénieurie liés aux langages de programmation, aux spécificités métiers
+ ou à la dette technique. La société est engagée dans l'*open source*
+ et contribue aux langages Rust, WebAssembly et OCaml. La société développe
+ aussi le prouveur SMT Alt-Ergo utilisé dans DéCySif.
+ OCamlPro est également active dans le domaine de la certification
+ Critères Communs au niveau EAL6 et l'utilisation des méthodes formelles
+ (Coq, Lean4, Why3)."
+
+
+ - name: "TrustInSoft"
+ url: "https://trust-in-soft.com/"
+ description:
+ "TrustInSoft commercialise des outils et services d'analyse exhaustive de
+ code source C et C++ permettant d'apporter des garanties mathématiques sur
+ la qualité des logiciels de ses clients. Ces solutions d'analyses de
+ logiciel permettent d'avoir des garanties sur la sécurité et la fiabilité
+ du code source sans modifier le processus de développement. Ces offres
+ sont déployées dans le monde entier chez les développeurs et intégrateurs
+ de composants logiciels issus des industries aéronautique, automobile,
+ ferroviaire, militaire, nucléaire, télécoms, ou l'IoT."
+
+software:
+ sectiontitle: "Les logiciels"
+---
diff --git a/content/fr/about.fr.md b/content/fr/about.fr.md
deleted file mode 100644
index 8ad23b4..0000000
--- a/content/fr/about.fr.md
+++ /dev/null
@@ -1,40 +0,0 @@
----
-title: "À propos"
-description: "Les acteurs du projet DéCySif"
-omit_header_text: true
-featured_image: '/images/Decysif.png'
-type: page
-menu:
- main:
- weight: 2
----
-
-# Le projet
-
-Depuis quelques années, le langage de programmation Rust vient concurrencer les
-langages Ada/C/C++ établis dans le monde des logiciels critiques, embarqués ou
-non. Les acteurs actuels et futurs développant des
-logiciels critiques en Rust se posent désormais la question de l'opportunité
-d'utiliser des outils d’analyse formelle pour Rust.
-
-C'est pour répondre à cette question que l'outil Creusot pour Rust a été
-développé par l'INRIA. L'outil est basé sur les mêmes fondations technologiques
-que les outils d’analyse formelle d’AdaCore et de TrustInSoft : la plateforme
-Why3 développée par l'INRIA et les mêmes prouveurs automatiques dont le
-prouveur Alt-Ergo d'OCamlPro.
-
-Le projet DéCySif vie l'amélioration de tous ces outils afin de converger vers
-une solution optimale pour la sécurité et la sûreté des systèmes critiques.
-
-{{< figure src="/images/Organisation-outils.png" >}}
-
-# Le consortium
-
-{{< presentation >}}
-
-# Coordinateur
-
-La société TrustInSoft est le coordinateur du projet. Pour toute demande
-d'information, veuillez passer par le formulaire de
-[contact]({{< ref "contact.fr.md" >}}).
-
diff --git a/content/fr/contact.fr.md b/content/fr/contact.fr.md
index b714010..3f7e2b4 100644
--- a/content/fr/contact.fr.md
+++ b/content/fr/contact.fr.md
@@ -1,12 +1,13 @@
---
title: Contact
-featured_image: ''
+cascade:
+ featured_image: '/images/Decysif.png'
omit_header_text: true
description: "Laissez-nous un message!"
type: page
menu:
main:
- weight: 3
+ weight: 4
---
Pour nous contacter, merci de remplir le formulaire ci-dessous.
diff --git a/content/fr/post/_index.md b/content/fr/post/_index.md
index 1a67b47..436afc8 100644
--- a/content/fr/post/_index.md
+++ b/content/fr/post/_index.md
@@ -1,7 +1,6 @@
---
title: "Actualités"
date: 2017-03-02T12:00:00-05:00
-type: page
featured_image: '/images/Decysif.png'
---
Lisez toutes les dernières avancées du projet ici !
diff --git a/hugo.toml b/hugo.toml
index 788713c..5522602 100644
--- a/hugo.toml
+++ b/hugo.toml
@@ -30,3 +30,7 @@ Paginate = 10
recent_posts_number = 5
[params.contact]
development = "https://formspree.io/f/mayreylq"
+
+# Helps display HTML inlined inside of frontmatter variables
+[markup.goldmark.renderer]
+ unsafe = true
diff --git a/layouts/_default/baseof.html b/layouts/_default/baseof.html
new file mode 100644
index 0000000..52e7e67
--- /dev/null
+++ b/layouts/_default/baseof.html
@@ -0,0 +1,59 @@
+
+
+
+
+
+ {{/* NOTE: the Site's title, and if there is a page title, that is set too */}}
+ {{ block "title" . }}{{ with .Params.Title }}{{ . }} | {{ end }}{{ .Site.Title }}{{ end }}
+
+
+ {{ hugo.Generator }}
+ {{/* NOTE: For Production make sure you add `HUGO_ENV="production"` before your build command */}}
+ {{ $production := eq (getenv "HUGO_ENV") "production" | or (eq site.Params.env "production") }}
+ {{ $public := not .Params.private }}
+ {{ if and $production $public }}
+
+ {{ else }}
+
+ {{ end }}
+
+ {{ partial "site-style.html" . }}
+ {{ partial "site-scripts.html" . }}
+
+ {{ block "favicon" . }}
+ {{ partialCached "site-favicon.html" . }}
+ {{ end }}
+
+ {{ if .OutputFormats.Get "RSS" }}
+ {{ with .OutputFormats.Get "RSS" }}
+
+
+ {{ end }}
+ {{ end }}
+
+ {{ if .Params.canonicalUrl }}
+
+ {{ else }}
+
+ {{ end }}
+
+ {{/* NOTE: These Hugo Internal Templates can be found starting at https://github.com/gohugoio/hugo/tree/master/tpl/tplimpl/embedded/templates */}}
+ {{- template "_internal/opengraph.html" . -}}
+ {{- template "_internal/schema.html" . -}}
+ {{- template "_internal/twitter_cards.html" . -}}
+
+ {{ if eq (getenv "HUGO_ENV") "production" | or (eq .Site.Params.env "production") }}
+ {{ template "_internal/google_analytics.html" . }}
+ {{ end }}
+ {{ block "head" . }}{{ partial "head-additions.html" . }}{{ end }}
+
+
+
+
+ {{ block "header" . }}{{ partial "site-header.html" .}}{{ end }}
+
+ {{ block "main" . }}{{ end }}
+
+ {{ block "footer" . }}{{ partialCached "site-footer.html" . }}{{ end }}
+
+
diff --git a/layouts/index.html b/layouts/index.html
new file mode 100644
index 0000000..0b29bd0
--- /dev/null
+++ b/layouts/index.html
@@ -0,0 +1,86 @@
+{{ define "header" }}{{ partial "page-header.html" . }}{{ end }}
+{{ define "main" }}
+
+
+
+
+
+
+{{ end }}
diff --git a/layouts/page/single.html b/layouts/page/single.html
new file mode 100644
index 0000000..825db29
--- /dev/null
+++ b/layouts/page/single.html
@@ -0,0 +1,15 @@
+{{ define "header" }}{{ partial "page-header.html" . }}{{ end }}
+{{ define "main" }}
+
+
+
+
+ {{ .Title }}
+
+
+
+ {{ .Content }}
+
+
+
+{{ end }}
diff --git a/layouts/partials/func/GetFeaturedImage.html b/layouts/partials/func/GetFeaturedImage.html
new file mode 100644
index 0000000..8d250c7
--- /dev/null
+++ b/layouts/partials/func/GetFeaturedImage.html
@@ -0,0 +1,41 @@
+{{/*
+ GetFeaturedImage
+
+ This partial gets the url for featured image for a given page.
+
+ If a featured_image was set in the page's front matter, then that will be used.
+
+ If not set, this will search page resources to find an image that contains the word
+ "cover", and if found, returns the path to that resource.
+
+ If no featured_image was set, and there's no "cover" image in page resources, then
+ this partial returns an empty string (which evaluates to false).
+
+ @return RelPermalink to featured image, or an empty string if not found.
+
+*/}}
+
+{{/* Declare a new string variable, $linkToCover */}}
+{{ $linkToCover := "" }}
+{{ $matches := "feature,cover" }}
+{{/* Use the value from front matter if present */}}
+{{ with .Params.featured_image }}
+ {{/* This is the default case, the image lives in the static directory.
+ In which case we'll use the static dir */}}
+ {{ $linkToCover = trim . "/" | absURL }}
+ {{/* If we find a Page Resource matching the exact value, we use it instead. */}}
+ {{ with $.Resources.GetMatch . }}
+ {{ $linkToCover = .RelPermalink }}
+ {{ end }}
+{{/* Find the first image with 'cover' in the name in this page bundle. */}}
+{{ else }}
+ {{ with .Resources.ByType "image" }}
+ {{ with .GetMatch (printf "**{%s}*" $matches) }}
+ {{ $linkToCover = .RelPermalink }}
+ {{ end }}
+ {{ end }}
+{{ end }}
+
+{{/* return either a permalink, or an empty string. Note that partials can only have a single
+return statement, so this needs to be at the end of the partial (and not in the if block) */}}
+{{ return $linkToCover }}
diff --git a/layouts/partials/page-header.html b/layouts/partials/page-header.html
new file mode 100644
index 0000000..3891c45
--- /dev/null
+++ b/layouts/partials/page-header.html
@@ -0,0 +1,25 @@
+{{ $featured_image := partial "func/GetFeaturedImage.html" . }}
+{{ if $featured_image }}
+ {{/* Trimming the slash and adding absURL make sure the image works no matter where our site lives */}}
+
+
+ {{ partial "site-navigation.html" . }}
+
+ {{ if not .Params.omit_header_text }}
+
{{ .Title | default .Site.Title }}
+ {{ with .Params.description }}
+
+ {{ . }}
+
+ {{ end }}
+ {{ end }}
+
+
+
+{{ else }}
+
+
+ {{ partial "site-navigation.html" . }}
+
+
+{{ end }}
diff --git a/layouts/partials/site-header.html b/layouts/partials/site-header.html
new file mode 100644
index 0000000..1a0b3cb
--- /dev/null
+++ b/layouts/partials/site-header.html
@@ -0,0 +1,35 @@
+{{ $featured_image := partial "func/GetFeaturedImage.html" . }}
+{{ if $featured_image }}
+ {{/* Trimming the slash and adding absURL make sure the image works no matter where our site lives */}}
+
+
+ {{ partial "site-navigation.html" .}}
+
+
+ {{ .Title | default .Site.Title }}
+
+ {{ with .Params.description }}
+
+ {{ . }}
+
+ {{ end }}
+
+
+
+{{ else }}
+
+
+ {{ partial "site-navigation.html" . }}
+
+
+ {{ .Title | default .Site.Title }}
+
+ {{ with .Params.description }}
+
+ {{ . }}
+
+ {{ end }}
+
+
+
+{{ end }}
diff --git a/layouts/partials/site-navigation.html b/layouts/partials/site-navigation.html
index ae6e328..700c8e8 100644
--- a/layouts/partials/site-navigation.html
+++ b/layouts/partials/site-navigation.html
@@ -9,17 +9,37 @@
{{ partial "i18nlist.html" . }}
- {{ if .Site.Menus.main }}
+ {{ with .Site.GetPage "index.md" }}
- {{ end }}
{{ partialCached "social-follow.html" . }}
diff --git a/layouts/post/list.html b/layouts/post/list.html
new file mode 100644
index 0000000..c53b0c8
--- /dev/null
+++ b/layouts/post/list.html
@@ -0,0 +1,56 @@
+{{ define "header" }}{{ partial "page-header.html" . }}{{ end }}
+{{ define "main" }}
+
+ {{ .Content }}
+
+ {{/* Define a section to pull recent posts from. For Hugo 0.20 this will default to the section with the most number of pages. */}}
+ {{ $mainSections := .Site.Params.mainSections | default (slice "post") }}
+ {{/* Create a variable with that section to use in multiple places. */}}
+ {{ $section := where .Site.RegularPages "Section" "in" $mainSections }}
+ {{/* Check to see if the section is defined for ranging through it */}}
+ {{ $section_count := len $section }}
+ {{ if ge $section_count 1 }}
+ {{/* Derive the section name */}}
+ {{ $section_name := index (.Site.Params.mainSections) 0 }}
+
+
+ {{/* Use $section_name to get the section title. Use "with" to only show it if it exists */}}
+ {{ with .Site.GetPage "section" $section_name }}
+
+ {{ end }}
+
+ {{ $n_posts := $.Param "recent_posts_number" | default 3 }}
+
+
+ {{/* Range through the first $n_posts items of the section */}}
+ {{ range (first $n_posts $section) }}
+
+ {{ .Render "summary-with-image" }}
+
+ {{ end }}
+
+
+ {{ if ge $section_count (add $n_posts 1) }}
+
+
{{ i18n "more" }}
+ {{/* Now, range through the next four after the initial $n_posts items. Nest the requirements, "after" then "first" on the outside */}}
+ {{ range (first 4 (after $n_posts $section)) }}
+
+ {{ end }}
+
+ {{/* As above, Use $section_name to get the section title, and URL. Use "with" to only show it if it exists */}}
+ {{ with .Site.GetPage "section" $section_name }}
+ {{ i18n "allTitle" . }}
+ {{ end }}
+
+ {{ end }}
+
+
+ {{ end }}
+{{ end }}
diff --git a/layouts/post/summary.html b/layouts/post/summary.html
new file mode 100644
index 0000000..24e3581
--- /dev/null
+++ b/layouts/post/summary.html
@@ -0,0 +1,16 @@
+
+