-
Notifications
You must be signed in to change notification settings - Fork 10
Meeting 19.10.2016
Hans-Joerg has set up a test installation in a virtual machine and created a small Jenkinsfile to test Jenkins. We now plan to contact the IT service to get a VM with Jenkins. For this we need to know:
- How much network traffic is expected (size of repo * number of commits per week)
- From where should the VM be accessible (current suggestion: FU intern only)
- How is user access done.
- Who needs what kind of access. We plan to pursue this further in the upcoming weak.
Furthermore, we need to collect a set of benchmarks. The resources
folder needs some cleanup
Alex and Hans-Jörg discussed pattern unification. The algorithm described in "Functional Unification of Higher-Order Patterns" is very promising. Some adaption of implementation details of Leo-III will be necessary.
Alex did some refactoring. The main change is that signatures are not global anymore. The refactoring didn't have any negative impact. Everything works as well as before and might even be faster now.
This is part of a longer list of tasks that Alex is now working on one by one.
Alex discussed the challenges when solving unification constraints on clauses. Depending on the rule that generated the clause, different sets of literals might be preferably considered first. This used to be solved in an ad-hoc way using flags, which broke at some point in the past. This will now be replaced with a clean and future save implementation.
After the sequential loop, Max now separated unification too. The performance looks promising.
Furthermore, the scheduler queue now requests new tasks if it is bellow a certain threshold.