Weekly development report 2021-08-28

Welcome to the weekly development report or what was done in my Open Source projects in the last week. This week has more entries, caused by general "sparkification" of my code. :)

Steam Sky

Roguelike in a sky with steampunk theme (written in Ada)

They said that the best place to hide is plain sight. And I see some of my bugs know this rule. :) Just caught two of them, related to entering a wrong value in numeric fields, like amount items to buy or sell, etc. This mean that in around 24 hours since this post, a new, a bit more stable version of the game will be available to download.

The development version going forward in its own pace:

TASHY2

Ada binding to Tcl/Tk, the new version of TASHY

As promised in the last week. The whole this week was spent on adding various keysyms supported by the Tk library to Tk.Bind package. And here is still some work to do with it. But the main work in this week was focused on making the library more SPARK friendly. At this moment, it means adding default values in many records and fixing precondition contracts for various subprograms. A bit strange that GNAT doesn't detect the problems with preconditions. Also, unfortunately, the whole library will not be fully formally verified, mostly due to way how adding new Tcl commands is made. But the most specification should allow use it in SPARK code. Also, I will try to formally verify as much as possible of the code. For now as a main testing field is used the library demo program. The goal is that it should be almost fully SPARK ready. At this moment I'm trying different approach to the adding new Tcl commands in Tcl.Commands package. We will see if it works or not. Also, added some Bob commands to run verification a bit easier in console. And another GitHub workflow with checking the library with gnatprove. :)

Hunter

Graphical File Manager for Linux (written in Ada)

Work on clearing the program code and updating the console version of the program slowly moves forward, but unfortunately, due to work on Tashy, it almost stopped at the end of the week:

YASS

Yet Another Static Site (generator) (written in Ada)

Copy and paste from the previous week: fixing the problems reported by AdaControl continues. It is still at the Pages package. That going very slowly forward. But this time also the project documentation got some updates.

DockerAda

Various Docker images files related to the Ada programming language

The adabuild image was fixed with missing GPR_PROJECT_PATH environment variable. Also, added showing the progress of download of SPARK. And updated the project documentation with information about the contents of the adabuild image.

TASHY

Ada binding to Tcl/Tk, based on TASH

After almost one year of break, this project is back to life again. :) Main reason is try to formally verify Steam Sky. This requires to make Tashy a more SPARK-friendly. The whole library will be never formally verified, probably only Tk bindings' specification will be checked for SPARK correctness. But even this should help a little. At this moment only few packages are 100% sure that work with a SPARK code, still more work to do. Also added function Arguments_To_Array which allows convert C arguments of Tcl commands to Ada array of Unbounded_Strings. But the most important information is that this version will contain possibly breaking change: the type Tcl_Interpreter was changed from a pointer to System.Address so it can now work with a SPARK code.

Back