1 points par GN⁺ 2024-12-28 | 1 commentaires | Partager sur WhatsApp
  • Quiver est un éditeur permettant de créer graphiquement des diagrammes commutatifs et des diagrammes de recollement, avec un rendu de haute qualité pour l’écran et l’export vers LaTeX et Typst
  • La création et la modification de diagrammes y sont bien plus rapides que l’écriture manuelle en LaTeX ou Typst ; une fois l’outil maîtrisé, le rythme de travail peut se rapprocher de celui du stylo et du papier
  • Il permet de gérer des diagrammes complexes comme les pullbacks, pushouts, adjunctions et higher cells, et propose une grille flexible qui s’adapte à la taille des labels ainsi que des styles de flèches composables
  • Il est possible de travailler aussi bien par glisser-déposer à la souris qu’avec des raccourcis clavier, avec sélection multiple, annulation/rétablissement, macros utilisateur, export de diagrammes intégrables en HTML, panoramique et zoom
  • Lors de l’export vers LaTeX ou Typst, un lien vers le diagramme est inséré afin de pouvoir le rouvrir plus tard pour le modifier ou le partager avec d’autres

Ce que fait Quiver

Fonctionnalités de création de diagrammes

  • Fournit une interface efficace et intuitive pour créer des diagrammes commutatifs complexes et des diagrammes de recollement
  • Exemples pris en charge :
    • diagrammes incluant des pullbacks et des pushouts
    • adjunctions
    • higher cells
  • Le placement des objets repose sur une grille flexible qui s’ajuste à la taille des labels
  • Les flèches peuvent combiner différents styles
  • Les labels et les flèches peuvent utiliser des couleurs
  • L’outil est conçu pour produire des résultats agréables en capture d’écran comme en export LaTeX ou Typst, aussi proches que possible du diagramme d’origine

Modes de saisie et flux d’édition

  • Les diagrammes peuvent être créés et modifiés par clic et glisser-déposer à la souris
  • Un ensemble de raccourcis clavier permet d’effectuer toutes les actions, rendant possible une édition centrée sur le clavier
  • Plusieurs éléments peuvent être sélectionnés en même temps afin d’appliquer rapidement et facilement des modifications en masse
  • Un système d’historique permet d’annuler et rétablir les actions
  • Le panoramique et le zoom sont pris en charge pour travailler sur de grands diagrammes
  • L’outil propose un alignement intelligent des labels et un décalage des arêtes

Export et réutilisation

  • Les diagrammes peuvent être exportés vers LaTeX ou Typst
  • Le résultat exporté contient un lien permettant de revenir au diagramme correspondant
    • Il peut être rouvert plus tard si des modifications sont nécessaires
    • Il peut être partagé avec d’autres personnes
  • L’export de diagrammes intégrables en HTML est également pris en charge
  • Les macros personnalisées peuvent être utilisées en collant l’URL d’un fichier contenant \newcommand
  • L’intégration avec les éditeurs est décrite dans la documentation Editor integration et dans le wiki Quiver

Build et conditions d’exécution

  • Depuis la ligne de commande, exécuter make, puis ouvrir src/index.html dans un navigateur pour vérifier le résultat du build
  • Si les versions de Make ou de Bash ne conviennent pas, il est possible de télécharger manuellement la dernière version de KaTeX et de la placer sous src/KaTeX/
  • Si le chemin de KaTeX est incorrect, une erreur de chargement de KaTeX se produit
  • Quiver doit être exécuté via localhost
  • Si Python est installé, exécuter make serve dans le répertoire de Quiver, puis ouvrir localhost:8000 dans le navigateur
  • En cas de problème de build, il est possible d’ouvrir une issue GitHub en décrivant le problème

1 commentaires

 
GN⁺ 2024-12-28
Avis sur Hacker News
  • Cet outil est vraiment excellent. J’ai pu réaliser le cube de Fourier-Poisson [0] en une dizaine de minutes, et l’interface est très intuitive.
    Le choix de conception consistant à se concentrer sur les diagrammes commutatifs plutôt que sur un canevas libre me semble excellent : cela rend l’outil clair et facile à utiliser. Si j’avais eu ça au moment d’écrire mon article, j’aurais probablement gagné énormément de temps.
    [0] https://q.uiver.app/#q=WzAsOCxbMCwxLCJnIFxcdGV4dHsgb24gfVxcb...

    • Pour ceux que cela intéresse, A First Course in Fourier Analysis de Kammler semble être la référence.
  • Dans le même esprit, cet éditeur de réseaux de Petri récent m’a pas mal impressionné : https://pes.vsb.cz/petrineteditor/#/model
    Les réseaux de Petri sont géniaux. Si l’on transformait une machine à états finis en version multithread, cela ressemblerait à peu près à ça.
    J’ai découvert les réseaux de Petri pour la première fois en lisant des textes d’une organisation appelée « statebox ». Statebox s’intéressait aux réseaux de Petri, aux diagrammes commutatifs et à plusieurs notions de théorie des catégories ; après avoir lu quelques articles, j’ai été fasciné et travailler là-bas est devenu un rêve. Malheureusement, leur page d’accueil actuelle ne contient plus que la phrase « imagine being a category theorist » et un emoji qui rit en pleurant, donc je ne sais pas ce qui s’est passé.

  • Il y a quelques jours, j’ai utilisé cet outil pour dessiner un diagramme simple [0] destiné à mon livre [1].
    Malheureusement, comme il est dédié à la théorie des catégories, il n’offre pas beaucoup de possibilités pour joliment styliser les nœuds, mais on peut bien sûr le faire avec LaTeX.
    [0] https://q.uiver.app/#q=WzAsNSxbMSw2LCJcXHRleHR7TmF0dXJhbCBEZ...
    [1] http://abstractionlogic.com

  • Hier soir, j’utilisais https://tikzcd.yichuanshen.de/, qui ressemble à une version avec moins de fonctionnalités de cet outil. Cela dit, il reste plutôt correct pour créer des diagrammes simples.

  • Pourrais-tu expliquer ce que sont un diagramme commutatif et un diagramme de recollement à un développeur logiciel modeste et pas particulièrement brillant ?
    L’article Wikipédia était trop abstrait pour être compris à un niveau de base [0]
    [0]: https://en.wikipedia.org/wiki/Commutative_diagram

    • C’est simplement une manière lisible d’écrire des équations entre des fonctions, ou d’autres choses qui se composent comme des fonctions.
      S’il y a f au-dessus de A → B, cela représente une fonction f qui prend une entrée de A et produit une sortie dans B.
      Un diagramme où A → B est f, puis B → C est g, et A → C est h, signifie g ∘ f = h, c’est-à-dire que faire f puis g revient au même que faire h. Comme on écrit en même temps le domaine et le codomaine de chaque fonction, il devient facile de voir si les fonctions sont composables, autrement dit si elles passent la vérification de types.
      Comme les chemins dans le diagramme eux-mêmes se composent comme des fonctions, cette notation s’emboîte très naturellement. Par exemple, l’associativité est intégrée à la notation elle-même : A→B→C→D est l’unique façon d’exprimer la composition de trois fonctions, et il est même impossible d’écrire une différence entre (f∘g)∘h et f∘(g∘h).
    • Un diagramme commutatif est un ensemble d’arêtes orientées entre des nœuds, autrement dit un graphe orienté, avec en plus l’affirmation que deux chemins quelconques qui partent du même nœud et arrivent au même nœud sont considérés comme équivalents, en un certain sens.
      En général, si l’on prend un multigraphe orienté, qu’on y ajoute une description indiquant quels chemins sont équivalents ou non, et que cette relation d’équivalence satisfait quelques propriétés de base, on appelle cela une catégorie. Ce concept apparaît très souvent en mathématiques, en logique abstraite, etc. Dans ce contexte, les diagrammes commutatifs sont utiles pour raisonner visuellement et rapidement sur l’équivalence des chemins.
    • Chaque majuscule est un type, et chaque minuscule est une fonction d’un type vers un autre. En suivant un chemin dans le diagramme, on peut décrire plusieurs appels de fonctions. Par exemple, suivre f puis g puis n représente n(g(f(a))). C’est cela, le diagramme ; et dire que le diagramme est commutatif signifie que deux chemins quelconques ayant le même point de départ et le même point d’arrivée donnent la même chose.
      Ainsi, n(g(f(•))), s(r(l(•))) et s(m(f(•))) sont tous des chemins de A vers C’, ainsi que des appels de fonctions ; puisque le diagramme est dit commutatif, tous ces chemins sont égaux.
      Les monomorphismes, épimorphismes et isomorphismes sont toutes des propriétés importantes des fonctions, qui permettent de « simplifier » certains termes des deux côtés d’une égalité. Par exemple, en général, de f(g(x))=f(h(x)), on ne peut pas conclure que g(x)=h(x). Si f peut être simplifiée de cette manière, on l’appelle un monomorphisme. De même, si dans g(f(x))=h(f(x)) on peut simplifier f pour obtenir g(x)=h(x), alors f est un épimorphisme. Un isomorphisme satisfait les deux propriétés. Grâce à ces propriétés, dans certaines situations, on peut « parcourir à l’envers » certaines parties d’un diagramme.
      Une forme de théorème qu’on rencontre en théorie des catégories ressemble à des exemples comme le five lemma[0] : « regardez ce diagramme. Si g est un épimorphisme et h un monomorphisme, alors f est un isomorphisme ». Autrement dit, si l’on sait qu’on peut simplifier d’un côté et de l’autre, on apprend qu’on peut aussi simplifier ailleurs.
      [0] https://en.wikipedia.org/wiki/Five_lemma

      Le five lemma dit que si les lignes sont des suites exactes, que m et p sont des isomorphismes, que l est un épimorphisme et que q est un monomorphisme, alors n est aussi un isomorphisme.

    • C’est une manière de montrer que deux chemins passant par un diagramme sont égaux en un certain sens. Les points aux coins sont des objets, et les flèches sont des morphismes.
      Pour simplifier, on peut voir les objets comme des types, et les flèches comme des fonctions entre types.
      On part du coin supérieur gauche et on suit deux chemins en vérifiant les types. Si le diagramme est correctement typé, on dit qu’il commute, et les deux chemins sont équivalents en un certain sens. Le sens précis dépend de nombreux détails que l’on omet ici.
    • Lire la définition d’une catégorie devrait aider. C’est très abstrait, mais comme il n’y a que quelques axiomes, c’est assez simple.
      Un exemple de catégorie est celle des « ensembles et fonctions ». Dans cette catégorie, tous les ensembles imaginables sont des objets, c’est-à-dire des nœuds, et toutes les fonctions imaginables entre deux ensembles quelconques sont des flèches entre ces deux ensembles.
      Donc si l’on prend une flèche de A vers B et une flèche de B vers C, puis qu’on les compose comme des fonctions, on obtient une fonction de A vers C.
      On peut voir un diagramme commutatif comme un sous-ensemble de toute la catégorie, dans lequel, entre deux ensembles X et Y, suivre tous les chemins dessinés et composer les flèches de chaque chemin donne la même fonction.
      Je n’ai jamais lu sur les catégories supérieures, donc je ne suis pas sûr pour les diagrammes de recollement, mais il est probable qu’ils généralisent cette idée d’une manière ou d’une autre.
  • Peut-on exporter dans un format adapté au Web ? Sans doute SVG. Si l’on fait tourner quiver sur localhost, partager un lien n’est pas une option.

  • Quand je suivais un cours de théorie des catégories il y a quelques années, Quiver était vraiment indispensable. L’UI était propre et intuitive, et les fonctionnalités suffisantes. Comparé au fait de se battre avec TikZ, il n’y avait pas photo.

  • Très bon produit. Avant, j’écrivais généralement le code TikZ à la main, et j’étais assez rapide, mais j’ai beaucoup oublié depuis ; pour les diagrammes commutatifs, celui-ci me semble donc très utile.

  • Il y a ici un outil de génération de code qui ne demande qu’à être créé.

  • J’ai utilisé Quiver plusieurs fois, et l’expérience a toujours été bonne. Bravo aux créateurs.