Minor fixes and suggestions for Intro to SPARK course

[filip-gajowniczek-adacore]

Some suggestions and fixes I came up with while reading this material.

[gusthoff]

Hello @filip-gajowniczek-adacore, the test results are indicating this error:

/home/runner/work/learn/learn/content/courses/intro-to-spark/chapters/04_State_Abstraction.rst:684:Unexpected indentation.

Would you mind correcting it?

[filip-gajowniczek-adacore]

Hello @filip-gajowniczek-adacore, the test results are indicating this error:

/home/runner/work/learn/learn/content/courses/intro-to-spark/chapters/04_State_Abstraction.rst:684:Unexpected indentation.

Would you mind correcting it?

Hi Gustavo :),

The error it is flagging isn't mean to be productionized; its an inline comment that I think should be addressed (either with a code change, a GitHub issue, or a disposition that its unnecessary).

So whatever way we decide to address this comment in a follow-up commit we should keep in mind to resolve this indentation issue.

[gusthoff]

I agree that, ideally, TODO items should be addressed as soon as possible. However, we might also decide to just integrate those todo items as comments. In fact, we have many todo items in the .rst file. Usually, they have this syntax:

.. todo::
   
    Description...

In any case, I still prefer to have the tests passing because we might be missing other issues in your changes. Also, it shouldn't be hard to fix them, so it'd be great if you could fix those comments using the syntax I've just mentioned above.

[filip-gajowniczek-adacore]

Not a problem for me to make the changes :) want to make sure I didn't come off that way.

I am on the same page with you now that these TODOs should be mergeable in case we leave them in and address them at a later date.

Thanks for providing the proper syntax to an .rst newbie like myself, I'll get those fixed up :)

[gusthoff]

Hey @filip-gajowniczek-adacore, thanks a lot for fixing those issues. The tests are passing now. I've just found a small thing (an empty line missing) that I commented. Apart from it, your corrections to the text look good. I'll ask @yannickmoy to give his opinion on the todo items...

[yannickmoy]

Thanks Filip for the comments! @gusthoff some fixes are needed about how the proof engine is used, as apparently now some proofs are attempted on the examples from previous sections. Probably some directive to reset the state of the cumulative source batch is missing?

[yannickmoy]

The difference is that the first assertion is proved, the second is not, see the comments in the code.

[filip-gajowniczek-adacore]

What confuses me here is what Assertion_Checked_By_The_Tool and what Assumption_Validated_By_Other_Means are.

I think these are placeholders for some sort of boolean assertion expressions?

[yannickmoy]

yes, the above are just placeholders for arbitrary boolean expressions :-)

[filip-gajowniczek-adacore]

I do think examples could be useful here.

What I didn't really understand after reading this section was what kinds of expressions can be used for Assertion_Checked_By_The_Tool and Assumption_Validated_By_Other_Means.

I definitely acknowledge this is a complex topic which I may not have devoted enough time to, thus the reader could be the issue here as well :-P

[yannickmoy]

There is an example below of ghost procedures, can you explain why it's not sufficient?

[filip-gajowniczek-adacore]

The thing that is missing here for me, is the connection between the Ghost procedure and the production code. In the example presented I don't understand when I would want to use the Ghost variable A and the Ghost procedure Increase_A.

I think some of the later examples (like example 3) make this link. However, as a first time reader, I found myself re-reading this particular section several times.

In my opinion, the organization could be improved, by moving something like example 3 into this section.

[yannickmoy]

indeed, this section only presents the technique of ghost procedures, not their usage. Feel free to suggest reorganisation, although we want to keep exercises at the end of each section.

[yannickmoy]

it is proven with the same options and SPARK Community 2021 on my laptop. Probably a difference of running time, I suggest to run this example with --level=2 instead of --level=0 to avoid this issue.

[gusthoff]

I suggest to run this example with --level=2 instead of --level=0 to avoid this issue.

Unfortunately, at the moment, we don't support changing the level for individual code examples — we could only change the level from 0 to 2 for all examples.

[gusthoff]

Thanks Filip for the comments! @gusthoff some fixes are needed about how the proof engine is used, as apparently now some proofs are attempted on the examples from previous sections. Probably some directive to reset the state of the cumulative source batch is missing?

Hello @yannickmoy, could you please provide me a list of affected code examples, so I know which ones I should focus on?

Just FYI: we don't use the code aggregator anymore, so resetting cannot be an issue here. Instead, we group code examples into "projects."

[yannickmoy]

@gusthoff that's the 3 comments that @filip-gajowniczek-adacore added with the text "The following code snippet attempts to analyze the previous example and needs to be fixed." I checked that indeed these snippets don't work anymore, for the reason Filip mentions. It's in chapter 3.

[gusthoff]

@gusthoff that's the 3 comments that @filip-gajowniczek-adacore added with the text "The following code snippet attempts to analyze the previous example and needs to be fixed." I checked that indeed these snippets don't work anymore, for the reason Filip mentions. It's in chapter 3.

Thanks, @yannickmoy, I'll take a look at them.

[gusthoff]

@filip-gajowniczek-adacore, I've just uploaded a change to this PR that should fix the proof issues that you've identified. Just let me know if they're OK now.

[filip-gajowniczek-adacore]

@gusthoff

The changes you made appear to have resolved the issue. The associated TODOs can be removed.

Good stuff :)