This regards the process of setting up a grader for the first time.
Some things are not mentioned in README.md or do not work as expected.
After following the instructions, I get the following when running ./judge prepare:
======================================================
pythonversion = python3.6
======================================================
Read config
port = 4714
isabelleversion = Isabelle2020
sessions = Pure
HOL
HOL-Library
HOL-Datastructures
======================================================
prepare isabelle preferences in: /var/lib/isabelle-grader/Isabelle2020/.isabelle/Isabelle2020
cp: cannot stat 'Isabelle2020/settings': No such file or directory
======================================================
Now copying setting to local ~/.isabelle/Isabelle2020/etc/settings
copy custom settings to '~/.isabelle/Isabelle2020/etc/settings'
cp: cannot stat 'Isabelle2020/settings': No such file or directory
======================================================
build sessions specified in: Pure
HOL
HOL-Library
HOL-Datastructures
---- build Pure -----
./prepareserver.sh: line 46: /home/ubuntu/Isabelle2020/bin/isabelle: No such file or directory
---- build HOL -----
./prepareserver.sh: line 46: /home/ubuntu/Isabelle2020/bin/isabelle: No such file or directory
---- build HOL-Library -----
./prepareserver.sh: line 46: /home/ubuntu/Isabelle2020/bin/isabelle: No such file or directory
---- build HOL-Datastructures -----
./prepareserver.sh: line 46: /home/ubuntu/Isabelle2020/bin/isabelle: No such file or directory
======================================================
copy heaps
cp: cannot stat '/home/ubuntu/.isabelle/Isabelle2020/heaps': No such file or directory
======================================================
copy startserverscript
======================================================
prepare checking files in folder: /var/lib/isabelle-grader/Isabelle2020
======================================================
setup new network namespace
ubuntu@swim1:~/repos/proving-contest-backends/Isabelle$ mv ~/bin/Isabelle2020/ ~
ubuntu@swim1:~/repos/proving-contest-backends/Isabelle$ sudo ./judge prepare
======================================================
pythonversion = python3.6
======================================================
Read config
port = 4714
isabelleversion = Isabelle2020
sessions = Pure
HOL
HOL-Library
HOL-Datastructures
======================================================
prepare isabelle preferences in: /var/lib/isabelle-grader/Isabelle2020/.isabelle/Isabelle2020
cp: cannot stat 'Isabelle2020/settings': No such file or directory
======================================================
Now copying setting to local ~/.isabelle/Isabelle2020/etc/settings
copy custom settings to '~/.isabelle/Isabelle2020/etc/settings'
cp: cannot stat 'Isabelle2020/settings': No such file or directory
======================================================
build sessions specified in: Pure
HOL
HOL-Library
HOL-Datastructures
---- build Pure -----
0:00:01 elapsed time
---- build HOL -----
0:00:02 elapsed time
---- build HOL-Library -----
^C*** Interrupt
---- build HOL-Datastructures -----
*** Undefined session(s): "HOL-Datastructures"
======================================================
copy heaps
======================================================
copy startserverscript
======================================================
prepare checking files in folder: /var/lib/isabelle-grader/Isabelle2020
======================================================
setup new network namespace
Cannot create namespace file "/var/run/netns/isabelle-server": File exists
ubuntu@swim1:~/repos/proving-contest-backends/Isabelle$ sudo ./judge prepare
======================================================
pythonversion = python3.6
======================================================
Read config
port = 4714
isabelleversion = Isabelle2020
sessions = Pure
HOL
HOL-Library
HOL-Datastructures
======================================================
prepare isabelle preferences in: /var/lib/isabelle-grader/Isabelle2020/.isabelle/Isabelle2020
cp: cannot stat 'Isabelle2020/settings': No such file or directory
======================================================
Now copying setting to local ~/.isabelle/Isabelle2020/etc/settings
copy custom settings to '~/.isabelle/Isabelle2020/etc/settings'
cp: cannot stat 'Isabelle2020/settings': No such file or directory
======================================================
build sessions specified in: Pure
HOL
HOL-Library
HOL-Datastructures
---- build Pure -----
0:00:01 elapsed time
---- build HOL -----
0:00:02 elapsed time
---- build HOL-Library -----
Building HOL-Library ...
Finished HOL-Library (0:07:11 elapsed time, 0:07:26 cpu time, factor 1.04)
0:07:16 elapsed time, 0:07:26 cpu time, factor 1.02
---- build HOL-Datastructures -----
*** Undefined session(s): "HOL-Datastructures"
======================================================
copy heaps
======================================================
copy startserverscript
======================================================
prepare checking files in folder: /var/lib/isabelle-grader/Isabelle2020
======================================================
setup new network namespace
Cannot create namespace file "/var/run/netns/isabelle-server": File exists
Problems that I see here:
~/.isabelle/Isabelle2020/etc/settings need not exist. We should document what our use case for it typically is.
`HOL-Datastructures': has this changed in Isabelle2020?
The last error happens, if you run the script multiple times
Now I run: ./judge start:
./judge start
======================================================
pythonversion = python3.6
======================================================
Read config
port = 4714
isabelleversion = Isabelle2020
pythonversion = python3.6
cat: serverPID: No such file or directory
error: list of process IDs must follow -p
Usage:
ps [options]
Try 'ps --help <simple|list|output|threads|misc|all>'
or 'ps --help <s|l|o|t|m|a>'
for additional help text.
For more details see ps(1).
started an Isabelle server (version=Isabelle2020) (PID=15944)
B) trying to update the server password in the config (need to wait for the server to start up)
1. try:
failed, try again
2. try:
failed, try again
3. try:
failed, try again
4. try:
failed, try again
5. try:
failed, try again
6. try:
failed, try again
7. try:
failed, try again
8. try:
failed, try again
9. try:
failed, try again
10. try:
failed, try again
11. try:
failed, try again
^C
A second, more patient attempt:
./judge start
======================================================
pythonversion = python3.6
======================================================
Read config
port = 4714
isabelleversion = Isabelle2020
pythonversion = python3.6
started an Isabelle server (version=Isabelle2020) (PID=15992)
B) trying to update the server password in the config (need to wait for the server to start up)
1. try:
failed, try again
2. try:
failed, try again
3. try:
failed, try again
4. try:
failed, try again
5. try:
failed, try again
6. try:
failed, try again
7. try:
failed, try again
8. try:
failed, try again
9. try:
failed, try again
10. try:
failed, try again
11. try:
failed, try again
12. try:
failed, try again
13. try:
failed, try again
14. try:
failed, try again
15. try:
failed, try again
16. try:
failed, try again
17. try:
failed, try again
18. try:
failed, try again
19. try:
failed, try again
20. try:
failed, try again
21. try:
failed, try again
22. try:
failed, try again
23. try:
failed, try again
24. try:
failed, try again
25. try:
failed, try again
26. try:
failed, try again
27. try:
failed, try again
28. try:
failed, try again
29. try:
failed, try again
failed to update password (strange :( )
C) starting poller now
started a poller (PID=16054)
At this point the poller picks up new submissions, but the Isabelle server for grading is down (server.log):
A) Starting server for Isabelle2020
===============
Thu Jun 25 08:30:40 UTC 2020
Starting Isabelle server (Isabelle2020)
Reading profile isabelle.profile
Error: invalid file Isabelle2020.tar.gz
Error: proc 15944 cannot sync with peer: unexpected EOF
Peer 15946 unexpectedly exited with status 1
Parent pid 15944, child pid 15946
A) Starting server for Isabelle2020
===============
Thu Jun 25 08:37:40 UTC 2020
Starting Isabelle server (Isabelle2020)
Reading profile isabelle.profile
Error: invalid file Isabelle2020.tar.gz
Error: proc 15992 cannot sync with peer: unexpected EOF
Peer 15994 unexpectedly exited with status 1
Parent pid 15992, child pid 15994
The latter issue could be fixed by renaming Isabelle2020_linux.tar.gz to Isabelle2020.tar.gz and running prepare again.
Watchdog instructions: I do not understand what NAME refers to, and why we copy things around and which exactly.
This regards the process of setting up a grader for the first time. Some things are not mentioned in
README.mdor do not work as expected.After following the instructions, I get the following when running
./judge prepare:Problems that I see here:
~/.isabelle/Isabelle2020/etc/settingsneed not exist. We should document what our use case for it typically is.Now I run:
./judge start:A second, more patient attempt:
At this point the poller picks up new submissions, but the Isabelle server for grading is down (
server.log):The latter issue could be fixed by renaming
Isabelle2020_linux.tar.gztoIsabelle2020.tar.gzand runningprepareagain.Watchdog instructions: I do not understand what
NAMErefers to, and why we copy things around and which exactly.