Merge pull request #3 from ImperialCollegeLondon/blueprint

Misc fixes to the blueprint per requested

.gitignore

@@ -4,3 +4,6 @@
 .lake/*
 .DS_Store
 blueprint/print/print.log
+blueprint/web/
+blueprint/print/
+blueprint/src/*.paux

README.md

@@ -1,5 +1,7 @@
 # Fermat's Last Theorem
 
+[![Website](https://img.shields.io/badge/Website-ready-green)](https://ImperialCollegeLondon.github.io/FLT/) [![Documentation](https://img.shields.io/badge/Documentation-passing-green)](https://ImperialCollegeLondon.github.io/FLT/docs/) [![Blueprint](https://img.shields.io/badge/Blueprint-WIP-blue)](https://ImperialCollegeLondon.github.io/FLT/blueprint/) [![Paper](https://img.shields.io/badge/Paper-WIP-blue)](https://ImperialCollegeLondon.github.io/FLT/blueprint.pdf)
+
 An ongoing multi-author open source project to formalise a proof of Fermat's Last Theorem in the Lean theorem prover. 
 
 # Information about the project

blueprint/tasks.py

@@ -46,15 +46,33 @@ def web(ctx):
  os.chdir(cwd)
 
 @task
-def serve(ctx, random_port=False):
+def serve(ctx, port=8080, random_port=False):
+ """
+ Serve the blueprint website assuming the blueprint website is already built
+ """
+
+ class MyTCPServer(socketserver.TCPServer):
+ def server_bind(self):
+ import socket
+ self.socket.setsockopt(socket.SOL_SOCKET, socket.SO_REUSEADDR, 1)
+ self.socket.bind(self.server_address)
+
  cwd = os.getcwd()
  os.chdir(BP_DIR/'web')
- Handler = http.server.SimpleHTTPRequestHandler
+
  if random_port:
  port = random.randint(8000, 8100)
- print("Serving on port " + str(port))
- else:
- port = 8000
- httpd = socketserver.TCPServer(("", port), Handler)
- httpd.serve_forever()
+
+ Handler = http.server.SimpleHTTPRequestHandler
+ httpd = MyTCPServer(('', port), Handler)
+
+ try:
+ (ip, port) = httpd.server_address
+ ip = ip or 'localhost'
+ print(f'Serving http://{ip}:{port}/ ...')
+ httpd.serve_forever()
+ except KeyboardInterrupt:
+ pass
+ httpd.server_close()
+
  os.chdir(cwd)

docs/index.md

@@ -16,4 +16,6 @@ An ongoing multi-author open source project to formalise a proof of Fermat's Las
 
 The project is currently being led by Kevin Buzzard. It is funded by [grant EP/Y022904/1](https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y022904/1), awarded by the UK's Engineering and Physical Sciences Research Council. The project is hosted at Imperial College London. Kevin would like to extend many many thanks to both of these institutions for their ongoing support of this nonstandard research.
 
-General information ("What is Fermat's Last Theorem/Lean?" / "Why are you doing this?" etc) is [here](GENERAL.md).
+General information ("What is Fermat's Last Theorem/Lean?" / "Why are you doing this?" etc) is [here](https://github.com/ImperialCollegeLondon/FLT/blob/main/GENERAL.md).
+
+