Re: Isabelle

> Le 21 avr. 2026 à 00:14, Coralie <[email protected]> a écrit :
> 
> 
> 
> 
>> Il s'agit de l'assistant de preuve https://isabelle.in.tum.de/
>> 
>> La France peut s'enorgueillir de déveloper un compétiteur:
>> https://rocq-prover.org/
> 
> Je ne vois nulle part d'information sur les licences.
> 
> Si quelqu'un peut éclairer ma chandelle.

Étrangement la réponse est dans la page Wikipédia (https://fr.wikipedia.org/wiki/Rocq_(logiciel)) :
« C'est un logiciel libre <https://fr.wikipedia.org/wiki/Logiciel_libre> distribué selon les termes de la licence GNU LGPL <https://fr.wikipedia.org/wiki/Licence_publique_g%C3%A9n%C3%A9rale_limit%C3%A9e_GNU>. »

> 
>> NB: le logiciel libre RefPerSys que je dévelope pourrait devenir un
>> compétiteur de plus. Il est multi-threadé
>> 
> Sincèrement 
> 💌 Coralie 💌
> 

-- 
Pierre Malard
https://plm4-photos.odexpo.com

Clé OpenGPG : https://keys.openpgp.org <https://keys.openpgp.org/>

   « Je n'ai jamais séparé la République des idées de
      justice sociale, sans laquelle elle n'est qu'un mot »

                                                Jean Jaures - 1887

   |\      _,,,---,,_
   /,`.-'`'    -.  ;-;;,_
  |,4-  ) )-,_. ,\ (  `'-'
 '---''(_/--'  `-'\_)   πr

perl -e '$_=q#: 3|\ 5_,3-3,2_: 3/,`.'"'"'`'"'"' 5-.  ;-;;,_:  |,A-  ) )-,_. ,\ (  `'"'"'-'"'"': '"'"'-3'"'"'2(_/--'"'"'  `-'"'"'\_): 24πr::#;y#:#\n#;s#(\D)(\d+)#$1x$2#ge;print'