[im3w1l]

Yeah, I see this as a very interesting reply to the TLA+ post. Might spend my evening diving into Ada and Spark.

Edit: Some things I noticed. The package gnat-12 does not have gnatprove. Ada mode for emacs requires a compilation step that failes with gnat community edition. With alire there is no system gnat so it cannot compile it (quite possible I'm missing something). In the end I gave up on using emacs. Gnatstudio wouldn't run for me until I realized it needed ncurses. It also had some unhandled exceptions for me (raised PROGRAM_ERROR : adjust/finalize raised GNATCOLL.VFS.VFS_INVALID_FILE_ERROR: gnatcoll-vfs.adb:340), but in the end I managed to get it up and running.

Edit2: After playing around with it, I'm extremely impressed with what spark can do. I made a function to add 7 to numbers. Tried putting a post condition that the return value is bigger than input. "Nuh uh, it could overflow". Ok so I add a pre condition that numbers must be less than 100. "Uhm, buddy you are passing in 200 right there". This is useful stuff for real and easy to write too.

[yannickmoy]

you can ask Alire to install the latest GNAT it built, or to use another version installed on your machine, see https://alire.ada.dev/transition_from_gnat_community.html

It also explains how to install GNATprove: ``alr with gnatprove``

[im3w1l]

Sorry if it was confusing I kind of jumped between the issues I had with various approaches. I did manage to get gnatprove through alire through just that command, it was the apt gnat that didnt have gnatprove. What I wasn't sure how to correctly do with the alire install was

  cd ~/.emacs.d/elpa/ada-mode-i.j.k
  ./build.sh
  ./install.sh

Actually I didn't get that working with any of the options I tried I guess.