Move publication data to JSON and use Jekyll.

[rlepigre]

This is a first step towards improving the web page and making it easier to modify using Jekyll. The main changes are:

• Use a JSON file (_data/publications.json) to record all publication data, that is the file that will need to be modified to add a new publication.
• Use a template to generate the actual publication list from the JSON data.
• Update the instructions in the README.md to explain how to build the web page locally and how to add a publication.

I'm pretty sure that if we merge this GitHub pages will automatically take care of generating all the static files, however I have not attempted this before. Has anyone done that before? @RalfJung maybe?

Note that the JSON format I designed might not be exactly what we want in the long run, but I'd still merge this quickly because constructing this data (semi-automatically) once was annoying enough. The format can easily be changed by processing the file with the script.

[RalfJung]

I'm pretty sure that if we merge this GitHub pages will automatically take care of generating all the static files, however I have not attempted this before. Has anyone done that before? @RalfJung maybe?

I don't use GitHub pages, so -- no idea. What do the docs say?^^

[rlepigre]

I don't use GitHub pages, so -- no idea. What do the docs say?^^

My interpretation is that this should just work, but I'd like someone to confirm so that there is less chance of taking the site down. :)

[rlepigre]

But, well, the worst case scenario is that the list of publication disappears until we fix things. All the rest should still be viewable since browser are still able to display invalid HTML mostly correctly.

[rlepigre]

I ported my personal webpage to Jekyll in a similar way (https://github.com/rlepigre/rlepigre.github.io), and everything works out of the box. So we can just merge if everyone agrees.

[RalfJung]

I have generated the site locally and diff'd the html. I think some differences are not intended. Also the template has a <br/> after the conference name, which makes the diff much bigger than it has to be; can you remove that for now?

Something odd is going on with the mtac paper:

-          <dt>Mtac2: Typed Tactics for Backward Reasoning in Coq</dt>
+          <dt>
+            Section 5 contains a case study using the Iris Proof Mode.
+            
+          </dt>
           <dd>
             <div class="entry">
             Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer<br/>
-              <small class="text-muted">In ICFP 2018: ACM SIGPLAN International Conference on Functional Programming</small>
-              <br/>
-                   <small class="text-muted">Section 5 contains a case study using the Iris Proof Mode.</small>
+              <small class="text-muted">In ICFP 2018: ACM SIGPLAN International Conference on Functional Programming</small><br/>
+              
               <div class="buttons">

In the PhD dissertations, the dates got lost, and Siddharth even lost the institute:

               Siddharth Krishna<br/>
-              <small class="text-muted">New York University, September 2019</small>
+              <small class="text-muted">, </small>
               <div class="buttons">

For transfinite Iris, the links changed:

               <div class="buttons">
-                <a href="https://iris-project.org/pdfs/2020-transfinite-iris-submission.pdf" class="btn btn-outline-primary btn-sm">[preprint] .pdf</a>
-                <a href="https://iris-project.org/transfinite-iris/" class="btn btn-outline-primary btn-sm">website</a>
+                
+                <a href="https://iris-project.org/pdfs/2020-transfinite-iris-submission.pdf" class="btn btn-outline-primary btn-sm">.pdf</a>
+                
+                
+                
+                <a href="https://iris-project.org/transfinite-iris/" class="btn btn-outline-primary btn-sm">Website</a>
+                
                 <a href="https://gitlab.mpi-sws.org/iris/transfinite" class="btn btn-outline-primary btn-sm">Coq development</a>

Also for RefinedC:

-                <a href="https://plv.mpi-sws.org/refinedc/paper.pdf" class="btn btn-outline-primary btn-sm">[preprint] .pdf</a>
-                <a href="https://plv.mpi-sws.org/refinedc/" class="btn btn-outline-primary btn-sm">website</a>
+                
+                <a href="https://plv.mpi-sws.org/refinedc/paper.pdf" class="btn btn-outline-primary btn-sm">.pdf</a>
+                
+                
+                
+                <a href="https://plv.mpi-sws.org/refinedc/" class="btn btn-outline-primary btn-sm">Website</a>
+                
                 <a href="https://gitlab.mpi-sws.org/iris/refinedc" class="btn btn-outline-primary btn-sm">Coq development</a>

And for Actris2:

               <div class="buttons">
-                <a href="pdfs/2020-actris2-submission.pdf" class="btn btn-outline-primary btn-sm">[preprint] .pdf</a>
+                
+                <a href="pdfs/2020-actris2-submission.pdf" class="btn btn-outline-primary btn-sm">.pdf</a>

And for reloc reloaded:

               <div class="buttons">
-                <a href="pdfs/2021-reloc-reloaded-submission.pdf" class="btn btn-outline-primary btn-sm">[preprint] .pdf</a>
-                <a href="https://iris-project.org/reloc/" class="btn btn-outline-primary btn-sm">website</a>
+                
+                <a href="pdfs/2021-reloc-reloaded-submission.pdf" class="btn btn-outline-primary btn-sm">.pdf</a>
+                
+                
+                
+                <a href="https://iris-project.org/reloc/" class="btn btn-outline-primary btn-sm">Website</a>

And for all the "Case studies, ...", something like this happened:

-                <a href="pdfs/2017-case-study-verifying-dartino-framework.pdf" class="btn btn-outline-primary btn-sm">.pdf</a>
+                
+                
+                <a href="pdfs/2017-case-study-verifying-dartino-framework.pdf" class="btn btn-outline-primary btn-sm">Pdf</a>

-                <a href="https://lirias.kuleuven.be/bitstream/123456789/555709/1/CoqPL.pdf" class="btn btn-outline-primary btn-sm">abstract</a>
+                
+                
+                <a href="https://lirias.kuleuven.be/bitstream/123456789/555709/1/CoqPL.pdf" class="btn btn-outline-primary btn-sm">Abstract</a>

-                <a href="https://www.youtube.com/watch?v=9Dyna88piek" class="btn btn-outline-primary btn-sm">talk on youtube</a>
-                <a href="https://people.mpi-sws.org/~jung/iris/talk-hope2015.pdf" class="btn btn-outline-primary btn-sm">slides</a>
+                
+                
+                <a href="https://www.youtube.com/watch?v=9Dyna88piek" class="btn btn-outline-primary btn-sm">Talk on Youtube</a>
+                
+                <a href="https://people.mpi-sws.org/~jung/iris/talk-hope2015.pdf" class="btn btn-outline-primary btn-sm">Slides</a>

Can you please make it so that there are no visible changes with this PR? We might want to change some things for consistency, but that is best not lumped together with a big refactor like this.

[rlepigre]

Thanks for all the comments @RalfJung! I minimised the diff between the generated index.html and the old one (using git diff --no-index --word-diff=color old_index.html _site/index.html), and I think it is in a pretty good state now.

There are still a few differences but they are mostly an artefact of the generation process. There are two exceptions:

• Your thesis was the only one without a direct link to the pdf, so I added one.
• One pdf turned into .pdf (which is consistent with everywhere else).

The main problem is that there are loads of extra spaces. I can't seem to find how to remove these in a satisfactory way (using https://shopify.github.io/liquid/basics/whitespace/): either I make the template unreadable, or I make the generated HTML aweful.

[RalfJung]

Yeah I am not bothered the whitespace changes.

Thanks for the patches! I'll check this again later.

[rlepigre]

Yeah I am not bothered the whitespace changes.

I guess it is not such a big deal, but I really hate having lines containing only spaces.

[RalfJung]

Yeah, diif looks good now. So, as far as I am concerned we can land this. @robbertkrebbers what do you think?

[RalfJung]

Okay, let's see if the deployment works!