Difference between revisions of "2021.07.27"
Jump to navigation
Jump to search
| (6 intermediate revisions by the same user not shown) | |||
| Line 27: | Line 27: | ||
** Debian 10 cannot download cvc3 | ** Debian 10 cannot download cvc3 | ||
* Found medium article [https://medium.com/software-safety/introduction-to-tla-model-checking-in-the-command-line-c6871700a6a2], which connects to github[https://github.com/pmer/tla-bin]. | * Found medium article [https://medium.com/software-safety/introduction-to-tla-model-checking-in-the-command-line-c6871700a6a2], which connects to github[https://github.com/pmer/tla-bin]. | ||
** Download and try a simple tla file on dev.xlp.pub. | ** Download and try a simple tla file on dev.xlp.pub. | ||
** successfully use pcal, tlc, any, but failed to use tlatex [https://github.com/pmer/tla-bin/issues/10] | |||
* Installed kframework/kore [https://github.com/kframework/kore] | |||
==Conclusion== | ==Conclusion== | ||
[[Category:Daily Document]] | [[Category:Daily Document]] | ||
https://thewiki.us/index.php/Namespace_Management#Namespace_Management_Rules_in_PKC | https://thewiki.us/index.php/Namespace_Management#Namespace_Management_Rules_in_PKC | ||
== Tomorrow's work plan (to discuss) == | |||
* Now I have kore, tla, docker installed. What could be the next? | |||
* Run the dev.xlp.pub to thewiki.us workflow which secures thewiki.us deployment. | |||
== The activity in near future == | |||
* I think Ideation could have been practiced on PKC. To practice Ideation, we don't require a fancy interface but a specification for participants. By this way, we could demonstrate that it is the underlying structure which enhances Ideation. As we specify the proper structure and invite participants to execute, there will be data flowing in and we can extract the workflow, which could be streamlined and optimized afterwards. | |||
Latest revision as of 04:22, 28 July 2021
| Date | 2021-07-27 |
|---|---|
| Person | @KevinTung |
Context and Goal
- Found the containerized application of TLA and K-framework.
- 2021.07.26
To-Do
- Install and test TLA, K-Framework.
- Organize Meeting:2021.07.26/Ben,Kevin
- Run the dev.xlp.pub to thewiki.us workflow which secures thewiki.us deployment.
- Install IFrame which Jared requires and document the requirement in Application:dev.xlp.pub
- Report progress and mutual review.
Progress
- Namespace_Management
- Ideally, all the naming conventions should be configured here and the rules will apply to all the pages in the system.
- Finish Docker Workflow and need to test by other participants.
- How to account for their testing? User feedback?
- Fix the Dockerfile in [1]
- Changed the version of image to Debian:10
- Debian 10 cannot download cvc3
- Found medium article [2], which connects to github[3].
- Download and try a simple tla file on dev.xlp.pub.
- successfully use pcal, tlc, any, but failed to use tlatex [4]
- Installed kframework/kore [5]
Conclusion
https://thewiki.us/index.php/Namespace_Management#Namespace_Management_Rules_in_PKC
Tomorrow's work plan (to discuss)
- Now I have kore, tla, docker installed. What could be the next?
- Run the dev.xlp.pub to thewiki.us workflow which secures thewiki.us deployment.
The activity in near future
- I think Ideation could have been practiced on PKC. To practice Ideation, we don't require a fancy interface but a specification for participants. By this way, we could demonstrate that it is the underlying structure which enhances Ideation. As we specify the proper structure and invite participants to execute, there will be data flowing in and we can extract the workflow, which could be streamlined and optimized afterwards.