2021.07.27

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.