Build systems for teaching · Teaching [with] Coq

Inspired by this topic, maybe would make sense to look at "Coq build systems for teaching". The only build system I know that should be completely cross-platform is the one built into ProofGeneral

Ralf Jung (Sep 13 2023 at 14:00):

how does the installation for that work on windows? you somehow need emacs and then PG in emacs and then link that up with the coq binary?

Karl Palmskog (Sep 13 2023 at 14:01):

I didn't try personally, but there is an Emacs build for Windows without any Unix deps. That build works fine with MELPA/ELPA where PG can be found

Karl Palmskog (Sep 13 2023 at 14:02):

the problem is likely the path to Coq, yes, but that can be configured in .emacs. Students often do not like Emacs though

Ralf Jung (Sep 13 2023 at 14:02):

sounds like the first 2 weeks are spent to teach students emacs and then it's 4 weeks of teaching them coq and then the main course content can start... ;)

Ralf Jung (Sep 13 2023 at 14:03):

yeah emacs is a roadblock probably, though I'm concerned they wont like coqide much either. its not exactly on par with modern editors.

Ralf Jung (Sep 13 2023 at 14:04):

like, ideally coq-platform would ship with a fully configured vscode where the coq plugin is set up and just works (and supports multi-file projects)... that's my dream world ;)

Emilio Jesús Gallego Arias (Sep 13 2023 at 14:05):

jsCoq 1 included a prototype build system done by @Shachar Itzhaky , now jsCoq 2 and coq-lsp will soon include their own build system based in dune

Karl Palmskog (Sep 13 2023 at 14:07):

Pierre Rousselin (Sep 13 2023 at 14:24):

coqide works fine for me with undergraduate students, it's very simple. I might try jscoq

Ralf Jung (Sep 13 2023 at 14:31):

Pierre Rousselin (Sep 13 2023 at 14:32):

Ralf Jung (Sep 13 2023 at 14:36):

Ralf Jung (Sep 13 2023 at 14:37):

are .vo files portable? like, can we generate them with coq 8.17.1 on linux and then ship them to windows users with that exact same coq version? (yeah Im getting a bit desperate^^)

Gaëtan Gilbert (Sep 13 2023 at 14:38):

I think you would need to ship the stdlib with them, otherwise it will do the usual inconsistent assumptions error

Karl Palmskog (Sep 13 2023 at 14:39):

.vo files are tied to the OCaml compiler that produced them (is my understanding of OCaml's Marshal)

One option for you might be to produce a custom Coq Platform Windows installer with all .vo files students will use, then have them only edit/check a single file

Karl Palmskog (Sep 13 2023 at 14:39):

Pierre Rousselin (Sep 13 2023 at 14:43):

So your problem is with building .vo files on Windows, if I understand correctly?

Pierre Rousselin (Sep 13 2023 at 14:44):

Ralf Jung (Sep 13 2023 at 14:54):

I dont think that will work, students will have to edit files and import edited files.

Ralf Jung (Sep 13 2023 at 14:54):

my problem is that when you open the 2nd file in coqide and ask it to jump into the proof it says that it cannot import the first file

Ralf Jung (Sep 13 2023 at 14:55):

because something needs to build that .vo file. ideally that would happen transparently of course; on Linux/macOS we can use make by hand to work around that, on windows we can... make people suffer through the cygwin installer and then use make by hand, it seems.

Pierre Rousselin (Sep 13 2023 at 15:02):

This needs to be addressed, you are right... Indeed a WSL-based solution could work, but it would probably be better if it is handled directly by the IDE.

Ralf Jung (Sep 13 2023 at 15:26):

with WSL we need two coq installations, one in WSL and one on the host for coqide

Ralf Jung (Sep 13 2023 at 15:26):

or we run coqide inside WSL, but then we need a coq-platform-in-WSL installer...

Ralf Jung (Sep 13 2023 at 15:27):

for now we're going to try to use cygwin. the official cygwin installer is a total nightmare but the script in the coq platform seems to work pretty well and we might just take that script and adjust it a bit to remove the parts we dont need...

Paolo Giarrusso (Sep 13 2023 at 16:29):

Paolo Giarrusso (Sep 13 2023 at 16:30):

also I heard you don't like dune, but I understand it can be installed on Windows without Cygwin

Paolo Giarrusso (Sep 13 2023 at 16:34):

Not remotely: they embed hashes of dependencies, and Coq lacks reproducible builds (there's a GitHub ticket). IME rebuilding the same sources but reusing .vos almost ensures inconsistent assumptions errors (on large enough codebases)

Paolo Giarrusso (Sep 13 2023 at 16:35):

Ralf Jung (Sep 14 2023 at 09:25):

the linux installer is a snap package. snap in WSL seems to be highly experimental at best.

Ralf Jung (Sep 14 2023 at 09:26):

ah, did that change? last time I tried the vscode integration I couldnt find anything. something to consider for the next semester I guess. (or maybe during the semester, if we get enough complaints.^^)

Ralf Jung (Sep 14 2023 at 09:27):

Pierre Rousselin (Sep 14 2023 at 09:35):

I will try it out at home (I still have windows 10 on a machine). This needs to be addressed before any serious pedagogical discussions.

Paolo Giarrusso (Sep 14 2023 at 09:57):

Ralf: there ~~kinda~~ are three Coq vscode plugins: vscoq1 (coqide-like), vscoq2 (needs coq 8.18) and coq-lsp (more experimental? maybe also works with 8.17)

Paolo Giarrusso (Sep 14 2023 at 09:58):

Ralf Jung (Sep 14 2023 at 09:59):

Paolo Giarrusso (Sep 14 2023 at 10:00):

Michael Soegtrop (Sep 14 2023 at 10:39):

@Ralf Jung : again: if you need a more complete development environment on Windows, I would recommend cygwin. The setup of Coq via cygwin is highly automated and battle proven (in CI and several courses). You run a single command (after expanding a Coq platform scripts ZIP) and that's it. Installing WSL has a rather deep impact on a system and a lot of odd things can happen (I had my share of it). By contrast Installing cygwin doesn't do anything to your computer besides the files in the destination folder and 2 or 3 start menu shortcuts.

Ralf Jung (Sep 14 2023 at 11:26):

yeah currently we are leaning towards copying and adjusting your platform batch script to install enough of cygwin for things to work

Ralf Jung (Sep 14 2023 at 11:26):

so basically people will install the binary distribution of the platform for coqide, coqc, and the dependencies; and run that script for make (and the unix utilities required for the makefile)

Ralf Jung (Sep 14 2023 at 11:28):

I know cygwin paths can be problematic etc but when we tried this it worked good enough to run make and that's really all we need :shrug:

Michael Soegtrop (Sep 14 2023 at 11:49):

OK. as discussed in PC, an alternative would be a simple WIndows native solution based on coqmakefile + remake and possibly some 10 lines of C. But I think one can patch the templates of coqmakefile such that remake can handle the result with CMD as shell - and remake is trivial to supply on Windows.

Emilio Jesús Gallego Arias (Sep 14 2023 at 15:24):

coq-lsp does also work on windows from the native Shell, so that's quite an improvement for some. Indeed, our goal is to solve soon all the problems @Ralf Jung have found in teaching.

Michael Soegtrop (Sep 14 2023 at 15:25):

@Emilio Jesús Gallego Arias : do you know how the status of dune not requiring ocamlc at run time is?

Emilio Jesús Gallego Arias (Sep 14 2023 at 15:26):

@Michael Soegtrop there has been some progress on that, but still not released. Note tho that coq-lsp doesn't have this restriction.

Michael Soegtrop (Sep 14 2023 at 16:42):

@Emilio Jesús Gallego Arias : I am confused - I thought coq-lsp is "just" a language server. Can it build projects?

Emilio Jesús Gallego Arias (Sep 14 2023 at 16:47):

@Michael Soegtrop , yes, language servers can have this capability. In fact for Coq is very important, otherwise the current .vo model is very limited. I know things are a bit confusing, we are trying to improve the README, under the coq-lsp repos we have:

Ralf Jung (Sep 15 2023 at 07:08):

@Emilio Jesús Gallego Arias how does coq-lsp relate to vscoq2? Seeing our very sparse developer resources spread thin across multiple vscode plugins is quite concerning.

Karl Palmskog (Sep 15 2023 at 07:09):

Ralf Jung (Sep 15 2023 at 07:10):

Karl Palmskog (Sep 15 2023 at 07:11):

VsCoq2 is developed mainly by @Romain Tetley, an Inria research engineer who works with long-term backing from Inria

Ralf Jung (Sep 15 2023 at 07:12):

right... but as a user of either that means what? how do I decide which one to use? as a user I care little about the mode of development. I care about stability, maturity, features covered, ...

Karl Palmskog (Sep 15 2023 at 07:14):

Ralf Jung (Sep 15 2023 at 07:16):

I dont have a crystal ball so I cannot deduce from this information what the developers will prioritize

Ralf Jung (Sep 15 2023 at 07:16):

but it does seem like they are completely independent projects then and a lot of duplicated effort. :(

Ralf Jung (Sep 15 2023 at 07:17):

coq-lsp mentions opam in its installation instructions so that's already basically a no-go for teaching I think...^^ I guess it could eventually be packaged in the platform or so to avoid that issue?

Karl Palmskog (Sep 15 2023 at 07:25):

Emilio Jesús Gallego Arias (Sep 15 2023 at 09:02):

Indeed I tried to put coq-lsp in the platform but I'm unsure how to make that progress. Any help with that is very welcome, especially as coq-lsp has good windows support.

Michael Soegtrop (Sep 15 2023 at 09:16):

@Emilio Jesús Gallego Arias : as discussed offline coq-lsp was too late for the 2023.03 release and is planned for the 2023.09 release, which we started to build last week, but it will take 6..8 weeks. If coq-lsp is critically important, we can make a 2023.08.1 release, but building and signing the installers is a lengthy process, so it won't be in time for Ralf.

Michael Soegtrop (Sep 15 2023 at 09:16):

@Ralf Jung : as discussed I am working on a solution - we should concentrate on that.

Ralf Jung (Sep 15 2023 at 09:21):

Michael Soegtrop (Sep 15 2023 at 09:30):

I guess CoqIDE is very vintage to computer science students, but then vintage is "in" these days - you just have to sell it that way ;-)

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:12):

I'm unsure what "being a research project" means; coq-lsp is both a research project and something intended to be used widely by industrial and educational users; there are a lot of differences between both projects in terms of features, implementation, and development methodologies too.

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:13):

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:14):

Sure, for 2023.03 was too late, what I mean is that I don't understand what I need to do in terms of pull requests / code.

I'm happy to help with making a new release etc... but I need to get the package building in the CI first, this is the step I'm lost.

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:17):

I'd be happy even with an unsigned installer, I understand that there are some large teaching courses that intend to use coq-lsp this fall, and it works well for them, but they are distributing their own binaries to students which is a large load.

So if we can figure out how to build an unsigned installer that includes coq-lsp, we'd be happy to do the integration and testing work, so it is ready for the next release; also students can install an interim build easily.

Ralf Jung (Sep 15 2023 at 10:23):

last time I tried it it was way too slow for practical use. but that was many years ago.
does it support multi-file workspaces and all that? students need to have persistent data -- work on their files, save, get back to it.

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:33):

@Ralf Jung jsCoq 2.0 will support multi-file workspaces, as it is based on Flèche, but that won't ready until end-of-year I think, maybe sooner.

jsCoq "1.0" does support a single file, the support for multiple files that Shachar did I think is still a bit experimental.

So in jsCoq "1.0" you need to structure the classes in several html files, and have each file load the completed previous file.

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:33):

Ralf Jung (Sep 15 2023 at 11:11):

Sebastian Ertel (Sep 15 2023 at 11:20):

Hi there,
I use a Nix flake that can be extended to install (spac)emacs and all necessary proof general packages automatically.
The students would only need to install nix and then do a nix develop.
Would that be an option for you?

Ralf Jung (Sep 15 2023 at 11:26):

Sebastian Ertel (Sep 15 2023 at 11:31):

Ralf Jung (Sep 15 2023 at 11:33):

also from all I heard about nix, you need someone with nix experience on the team

Sebastian Ertel (Sep 15 2023 at 11:33):

Ralf Jung (Sep 15 2023 at 11:33):

so... the coq platform installer sounds a lot more appealing (even though Im not much of a snapd fan)

Emilio Jesús Gallego Arias (Sep 15 2023 at 12:11):

There is no cloud in jsCoq, it is just a bunch of html + js that you can run locally, or in a static web-server

Emilio Jesús Gallego Arias (Sep 15 2023 at 12:12):

Ralf Jung (Sep 15 2023 at 13:31):

Pierre Rousselin (Sep 18 2023 at 11:30):

I've tried using opam on WSL2 and so far it has been inconclusive, no idea why (coq-stdlib would not build). I will try again during the week with different methods.

Karl Palmskog (Sep 18 2023 at 11:31):

hmm, coq-stdlib has worked for me thus far in WSL2, but obviously the installation of the gmp system package via depext must succeed.

Pierre Roux (Sep 18 2023 at 11:32):

Pierre Rousselin (Sep 18 2023 at 11:32):

Karl Palmskog (Sep 18 2023 at 11:34):

coq-core/coq-stdlib depends on package zarith, and zarith depends on conf-gmp. gmp is a system package that can't be installed by opam directly (hinted at by the conf-). However, opam has a built-in system called depext that helps people install system libraries.

Karl Palmskog (Sep 18 2023 at 11:34):

the depext approach can work great or fail completely, depending on a number of factors

Karl Palmskog (Sep 18 2023 at 11:36):

on Ubuntu/WSL2, the system package is called libgmp-dev. So one thing to test is to manually run sudo apt install libgmp-dev before trying to install coq-core/coq-stdlib

Pierre Rousselin (Sep 18 2023 at 11:36):

Karl Palmskog (Sep 18 2023 at 11:36):

Karl Palmskog (Sep 18 2023 at 11:37):

I think by default it only uses 50% or something out of your system memory. I never had problems on a 16GB memory machine, but I can imagine an 8GB machine quickly runs out inside WSL2

Pierre Rousselin (Sep 18 2023 at 11:38):

It's actually possible since one of my memory card died and I'm on 8GB, though I would be surprised one can play diablo IV and cannot install Coq :D

Karl Palmskog (Sep 18 2023 at 11:40):

8GB at Windows level should work fine for Coq-in-Windows and lots of demanding games. But WSL2 cuts this by quite a lot, you can run top inside WSL2 and it should show 4GB or similar

Pierre Rousselin (Sep 18 2023 at 11:41):

Karl Palmskog (Sep 18 2023 at 11:43):

Michael Soegtrop (Sep 18 2023 at 16:39):

I just wanted to mention that the Coq Platform releases 2022.09.1 and 2023.03.0 contain an Addon zip file, which contains preliminary work on running coq_makefile and gnumake with CMD as shell. It does by far not support all features of coq_makefile yet, but the basic build rule for .vo files, Coq dependency file generation and the clean target work. For most lectures this should be good enough. This is delivered as ZIP file with two files (gnumake.exe and a patched template for coq_maefile) which are intended to copied over an installer generated installation. The plan is to integrate this in the next release.

Michael Soegtrop (Sep 18 2023 at 16:42):

So for plain Coq lectures, the Coq Platform installers should be fine now on all platform. For lectures also requiring OCaml, the compile from sources Coq Platform is recommended - possibly with a lecture specific pick.

Michael Soegtrop (Sep 18 2023 at 16:47):

Regarding WSL2: I would not use it for lectures. In my experience the average install effort is quite high and it has the problem that it does not work very well with other hypervisors. If people have VMware or VirtualBox installed, it might be substantial effort to get these working again. Besides I have seen quite a few strange things with WSL2, say blue screens not working any more (redirected to the hypervisor and ignored there). Also memory consumption can be an issue on laptops (half of 8 GB is quite on the edge for Coq work). IMHO WSL2 is fine for advanced personal work, but I would not ask 100 people to install it.

Ralf Jung (Sep 18 2023 at 16:51):

A huge thank you :heart: to @Michael Soegtrop for building this addon package on such short notice, this will be a great help. :)

Michael Soegtrop (Sep 18 2023 at 16:53):

Pierre Rousselin (Sep 23 2023 at 09:12):

(coqide:15208): dconf-WARNING **: 10:37:22.199: failed to commit changes to dconf: Could not connect: No such file or directory

Karl Palmskog (Sep 24 2023 at 12:34):

hmm... my guess would have been that WSL2 + Snap would be preferred over Debian pacakages (not least since Debian packages available on WSL2 would be several years out of date)

Pierre Rousselin (Sep 25 2023 at 08:41):

There are certainly advantages for using opam. For new Linux users however, installing distribution packages should be more natural.

Théo Zimmermann (Sep 25 2023 at 09:09):

Karl's suggestion above was not using opam (which would mean compiling from sources) but snap (which provides up-to-date prebuilt binaries). Cf. https://snapcraft.io/coq-prover

Pierre Rousselin (Sep 25 2023 at 09:14):

Michael Soegtrop (Sep 25 2023 at 16:40):

@Pierre Rousselin : my main critics on WSL is that if you install it all other VM systems (VMware, VirtualBox, variants of Qemu) stop working and it can be very hard to get them working again (WSL is easier to install than to fully get rid of). I am quite sure that if you ask 100 computer science students to install WSL, at least 10% won't be very grateful for the havoc this does to their working environment. Maybe this improved meanwhile - my latest tests are about 1 year ago. But definitely before you ask students to do this, you should check the interoperability with common VM systems and warn about side effects.

Pierre Rousselin (Sep 26 2023 at 14:08):

So finally the students all used wacoq. As an IDE it's incomplete, because the students can only save their snippets, not reload them. We had no problem with compiling or distributing anything yet because the first file was self-sufficient (it's here in french).

There were a couple of bugs, nothing critical, I noticed something like this when moving back and forth inside a proof:

Stm.add called for a different state (333) than the tip: 336.
This is not supported yet, sorry.

I don't think I will go back to CoqIDE because I noticed that the students have read the "comments" a lot more than during the previous editions. This made them really active during the course and some of them actually finished without any help. I really think a "Coq document for teaching" should be more than pure .v. That's the main reason for me for using jscoq or wacoq.

Emilio Jesús Gallego Arias (Sep 26 2023 at 14:37):

Emilio Jesús Gallego Arias (Sep 26 2023 at 14:40):

Note that we have a preview of jsCoq 2.0 here https://x80.org/rhino-down/ , if you click the "switch" button you can see this idea a bit better, and it also allows saving in a bit of better format

Théo Zimmermann (Sep 26 2023 at 14:52):

Thanks for the feedback Pierre! I agree that having more than a v file is certainly a good idea for teaching, and this is the reason why I've tried experimenting with coq-lsp to get the mv file support. This is very similar to what the jsCoq 2.0 demo linked above shows.

Pierre Rousselin (Oct 03 2023 at 16:55):

For the moment, jsCoq 1 suits more my needs than jsCoq 2 (in its current state, which if I'm correct should evolve). I like that the students directly have the html formatting of the "comments" and the proofs in code blocks without touching anything.
However, today, there was a need to load previous sessions. This is a real hindrance. It will be even more when I ask them to submit some homeworks.

I would like it a lot if someone could help me with this as I don't think I can teach myself that much of web programming in such a little time.

Emilio Jesús Gallego Arias (Oct 03 2023 at 16:57):

Yes that's a real PITA :( actually there could a very simple solution so have some sort of save / load that can be persisted to disk.

Emilio Jesús Gallego Arias (Oct 03 2023 at 16:58):

We already have the list of textareas that are used, so it is a one JS line we could generate a file that would contain an array of the raw contents; loading that back should be also trivial.

Pierre Rousselin (Oct 10 2023 at 15:00):

New session today. wacoq 16.0.0 does not like Set Printing Parentheses inside a proof.

Anomaly ""Assert_failure vendor/coq/stm/stm.ml:557:4"."
Please report at http://coq.inria.fr/bugs/.

Emilio Jesús Gallego Arias (Oct 10 2023 at 15:22):

Yes, unfortunately this bug is known and only fixed in jsCoq 2.0 ; it is due to a Coq bug. There is already an issue in the bug tracker.

Stream: Teaching [with] Coq

Topic: Build systems for teaching

Karl Palmskog (Sep 13 2023 at 13:59):

Ralf Jung (Sep 13 2023 at 14:00):

Karl Palmskog (Sep 13 2023 at 14:01):

Karl Palmskog (Sep 13 2023 at 14:02):

Ralf Jung (Sep 13 2023 at 14:02):

Ralf Jung (Sep 13 2023 at 14:03):

Ralf Jung (Sep 13 2023 at 14:04):

Emilio Jesús Gallego Arias (Sep 13 2023 at 14:05):

Karl Palmskog (Sep 13 2023 at 14:07):

Pierre Rousselin (Sep 13 2023 at 14:24):

Ralf Jung (Sep 13 2023 at 14:31):

Pierre Rousselin (Sep 13 2023 at 14:32):

Ralf Jung (Sep 13 2023 at 14:36):

Ralf Jung (Sep 13 2023 at 14:36):

Ralf Jung (Sep 13 2023 at 14:37):

Gaëtan Gilbert (Sep 13 2023 at 14:38):

Karl Palmskog (Sep 13 2023 at 14:39):

Karl Palmskog (Sep 13 2023 at 14:39):

Pierre Rousselin (Sep 13 2023 at 14:43):

Pierre Rousselin (Sep 13 2023 at 14:44):

Ralf Jung (Sep 13 2023 at 14:54):

Ralf Jung (Sep 13 2023 at 14:54):

Ralf Jung (Sep 13 2023 at 14:55):

Pierre Rousselin (Sep 13 2023 at 15:02):

Ralf Jung (Sep 13 2023 at 15:26):

Ralf Jung (Sep 13 2023 at 15:26):

Ralf Jung (Sep 13 2023 at 15:27):

Paolo Giarrusso (Sep 13 2023 at 16:29):

Paolo Giarrusso (Sep 13 2023 at 16:30):

Paolo Giarrusso (Sep 13 2023 at 16:30):

Paolo Giarrusso (Sep 13 2023 at 16:34):

Paolo Giarrusso (Sep 13 2023 at 16:35):

Ralf Jung (Sep 14 2023 at 09:25):

Ralf Jung (Sep 14 2023 at 09:26):

Ralf Jung (Sep 14 2023 at 09:27):

Pierre Rousselin (Sep 14 2023 at 09:35):

Paolo Giarrusso (Sep 14 2023 at 09:57):

Paolo Giarrusso (Sep 14 2023 at 09:58):

Ralf Jung (Sep 14 2023 at 09:59):

Paolo Giarrusso (Sep 14 2023 at 10:00):

Michael Soegtrop (Sep 14 2023 at 10:39):

Ralf Jung (Sep 14 2023 at 11:26):

Ralf Jung (Sep 14 2023 at 11:26):

Ralf Jung (Sep 14 2023 at 11:28):

Michael Soegtrop (Sep 14 2023 at 11:49):

Emilio Jesús Gallego Arias (Sep 14 2023 at 15:24):

Michael Soegtrop (Sep 14 2023 at 15:25):

Emilio Jesús Gallego Arias (Sep 14 2023 at 15:26):

Michael Soegtrop (Sep 14 2023 at 16:42):

Emilio Jesús Gallego Arias (Sep 14 2023 at 16:47):

Ralf Jung (Sep 15 2023 at 07:08):

Karl Palmskog (Sep 15 2023 at 07:09):

Ralf Jung (Sep 15 2023 at 07:10):

Karl Palmskog (Sep 15 2023 at 07:11):

Ralf Jung (Sep 15 2023 at 07:12):

Karl Palmskog (Sep 15 2023 at 07:14):

Ralf Jung (Sep 15 2023 at 07:16):

Ralf Jung (Sep 15 2023 at 07:16):

Ralf Jung (Sep 15 2023 at 07:17):

Karl Palmskog (Sep 15 2023 at 07:25):

Emilio Jesús Gallego Arias (Sep 15 2023 at 09:02):

Michael Soegtrop (Sep 15 2023 at 09:16):

Michael Soegtrop (Sep 15 2023 at 09:16):

Ralf Jung (Sep 15 2023 at 09:21):

Ralf Jung (Sep 15 2023 at 09:21):

Ralf Jung (Sep 15 2023 at 09:21):

Michael Soegtrop (Sep 15 2023 at 09:30):

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:12):

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:13):

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:13):

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:14):

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:17):

Ralf Jung (Sep 15 2023 at 10:23):

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:33):

Emilio Jesús Gallego Arias (Sep 15 2023 at 10:33):

Ralf Jung (Sep 15 2023 at 11:11):

Ralf Jung (Sep 15 2023 at 11:11):

Sebastian Ertel (Sep 15 2023 at 11:20):