Blogpost idea: “Tactics are Basically Procedural Macros”

With some examples of metaprogramming, compared to other languages such as Elixir or Lisp… or Rust if only I knew how to write macros in Rust :p

Not sure if it would work, will have to try to see

So. Like for my latest blogpost, I will use this thread for commenting on my next publication.

You can already find it here: soap.coffee/~lthms/posts/Tacti but it is a draft obviously.

I need to work on the presentation of this one for it to remain readable, I think.

Show thread
Follow

So, I think it is mostly ready. The focus has shifted, as the example I had in mind has proven to be harder to implement than anticipated.

Side note: I don’t think I have already read a similar write-up yet.

If the subject is of some interest for you, I am interested in your feedback prior to sharing it more vastly.

soap.coffee/~lthms/posts/Mixin

Thanks! and <3

@lthms La conclusion est sympa… mais je l’étendrait un petit peu. Typiquement, je n’ai aucune honte à utiliser des tactiques monstrueuses pour générer des termes de la forme { x | P x }… je pense même que c’est dans ce cas souhaitable ! ☺

@MartinShadok ahah j’y ai pensé ! Je vais rajouté ça, merci.

@lthms @MartinShadok je l’avais pas mis car dans le cas que tu cites, tu utilises auto&co pour générer la preuve de P x surtout, mais autant être explicite

@lthms Justement non ! Je l’utilise vraiment pour générer le x surtout ! ☺ C’est typiquement dans les cas où je sais qu’on peut construire un tel x, mais tant que le x respecte P x, je suis content de l’avoir (typiquement quand P est très restrictif ☺).

Un cas typique est cette définition : github.com/WasmCert/WasmCert-C (Voir son cas d’utilisation ici : github.com/WasmCert/WasmCert-C )

@lthms En fait, dès que tu as quelque chose de la forme { P } + { ~P }, tu es finalement en train de construire un booléen { b | reflect P b } 😊

@MartinShadok J’ai mis à jour en rajoutant un paragraphe, comme suggéré.

Du coup je pense que je vais le laisser reposer en l’état et le figer demain. Merci pour le retour !

@lthms Merci pour l'article ! 😀 C'est vachement intéressant 😊

@MartinShadok tu me diras ce qu’en a pensé ton étudiant ! (:

@MartinShadok Ça me fait penser qu’il faut vraiment que j’investisse du temps dans l’apprentissage de SSReflect, au moins pour ma culture générale…

@lthms Pour ce projet, c'est Jean Pichon qui l'avait proposé (sur le ton de « chiche ? »). On s'est tous dit que s'était une bonne occasion d'apprendre 😊 On n'a pas un style très très pur ssreflect, mais on s'en sort 😊 C'est effectivement bien fait ☺️

Après, c'est comme toutes les bibliothèques Coq : elle a été faite pour un usage finalement assez spécifique, et je la trouve un petit peu pauvre pour d'autres styles. Mais elle a été très bien faite 😊

Sign in to participate in the conversation
Mastodon

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!