Silence some warnings

• Currently we get two types of warnings during the compilation of Prosa
• One is to do with the use of deprecated tactics in elf/rta/bounded_pi.v. If we want to silence these warnings then we lose compatibility with Mathcomp 1.16
• The other is due to obligation tactics declared in behavior/schedule.v and behavior/ready.v
• Declaring this tactic does not actually solve any goals. However, it has the effect that the default Coq obligation tactic is not used and hence introsing of some variables is prevented.
• Currently I added the tactic back in local scope to the files where it is needed since otherwise it is not possible to generate proofs that are compatible with mangle names.
• However, maybe there is a better way of doing it.

added 1 commit

• 9a4c447e - change hack to be more idiomatic

Compare with previous version

marked this merge request as ready

Spellcheck ain't happy.

Is it possible to somehow constrain the Obligation Tactic command such that we can centralize it in a file in util.foo so that we can Require it in the various definition files, but without re-exporting it to any downstream code importing e.g. one of the processor models?

added 1 commit

• d187fa15 - make spell checker happy

Compare with previous version

BTW note that using idtac is a hack. Ideally, Coq should not have a tactic with global effects that makes it impossible to prove lemmas with mangle-names on

added 1 commit

• be53c714 - reword comment

Compare with previous version

added 1 commit

• 5e21ea45 - fix line break

Compare with previous version

added 1 commit

• 2217dd3b - change global behavior of obligation tactic

Compare with previous version

Can we get this merged in the next couple of days?

added 10 commits

• 2217dd3b...e3833b98 - 3 commits from branch RT-PROOFS:master
• 78e915f0 - silence some warnings
• a08b2583 - make obligation tactic local
• 61827dd8 - change hack to be more idiomatic
• ec40ba6b - make spell checker happy
• 4b5d7923 - reword comment
• 8e37352d - fix line break
• b850c983 - change global behavior of obligation tactic

Compare with previous version

added 1 commit

• 60048a4a - remove commented out code

Compare with previous version

added 1 commit

• 142ff8c1 - change comment

Compare with previous version

added 1 commit

• 12e24c92 - make spellchecker happy

Compare with previous version

resolved all threads

Looks good, thanks a lot for the cleanup!

approved this merge request

added 1 commit

• d13e4dbd - CI: remove mathcomp 1.16.0 job

Compare with previous version

assigned to @kbedarka

added 2 commits

• 4c651980 - undo wrong change
• 71e0c8c2 - Merge branch 'silencewarnings' of...

Compare with previous version

added 1 commit

• ee667398 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

approved this merge request

resolved all threads

enabled an automatic merge when the pipeline for ee667398 succeeds

merged