L’installation recommandée utilise maintenant le « paquet Python », voir cette page.
Cette page contient les versions « tout en un ». Pour la source, voir ici. En cas de problème sous Mac, voir ici.
- D∃∀DUCTION 0.3999
Nouveautés : corrections divers bugs, exercices élémentaires d’arithmétique
Instructions d’installation :
- Pour une installation légère sous Linux ou Mac, choisir le premier ou deuxième lien.
- Pas de version légère pour Windows pour le moment, utiliser la machine virtuelle.
- La machine virtuelle prend une place mémoire importante (autour de 30Go), mais permettra une mise à jour facile. Voici les instructions d’installation :
- Installez le logiciel Oracle VirtualBox VM sur votre système https://www.virtualbox.org/wiki/Downloads (si votre système est Linux et que vous ne tenez pas absolument a avoir la derniere version, il suffit de taper: sudo apt-get install virtualbox virtualbox-ext-pack)
- Téléchargez le fichier : Debian-ProofAssistants.ova
- Dans un explorateur de fichiers, faites un clic droit sur le fichier Debian-ProofAssistants.ova précédemment téléchargé et choisissez ‘Ouvrir avec Oracle VM VirtualBox’ Puis Cliquez sur ‘Importer’
- Dans le logiciel ‘Oracle VM VirtualBox’ cliquez sur la machine « Debian-ProofAssistants » (colonne de gauche) puis sur « Démarrer » (grosse flèche verte)
- Le login est ‘appam’ et le mot de passe est ‘anr’
- Double-cliquer sur le script ‘Deaduction.sh’ qui apparait sur le bureau virtuel
- D∃∀DUCTION 0.39
Nouveautés :
- Une « calculatrice logique » permet à l’utilisateurice de rentrer des objets mathématiques (pour appliquer un théorème, fournir un témoin pour démontrer une propriété existentielle, formuler un nouveau but, etc.)
- Nouvelle interface de choix des exercices, avec indication des exercices faits, et possibilité de sauvegarder les preuves.
- Boutons de calcul (expérimental) : additionner des inégalités, les enchainer, etc. .
- Amélioration de l’affichage des maths.
- Résolution de problèmes de ralentissement, ajout d’un bouton pour redémarrer le serveur Lean.
- D∃∀DUCTION 0.31
Nouveautés :
- Quelques exercices sur les limites !
- Correction de bugs, amélioration du choix des paramètres
- D∃∀DUCTION 0.3
Nouveautés :
- Aide sur chaque élément du contexte, et sur le but
- Glisser-déposer (« drag and drop »)
- D∃∀DUCTION 0.2
Nouveautés :
- Fenêtre donnant un aperçu global de la preuve
