Update the installation instructions. #125
Conversation
Fixes #123. Signed-off-by: Karolis Petrauskas <[email protected]>
|
@ahelwer, may I ask you to check if the installation-related changes in the documentation look good to you? |
|
Sure, I will test the installation docs tomorrow! For uploading the docs to the INRIA server what do you mean exactly? |
Docs from https://github.com/tlaplus/tlapm/tree/main/doc/web have to be published somehow at https://tla.msr-inria.inria.fr/tlaps/. That should be done in the CI (maybe on a release, not each commit). Such publishing is done for |
|
@kape1395 the docs website is now served using github pages from the main branch of this repo at https://proofs.tlapl.us |
|
@ahelwer, thanks for the update! Maybe you have reviewed the changes to the installation instructions? @lemmy, we should redirect somehow https://tla.msr-inria.inria.fr/tlaps/ to https://proofs.tlapl.us/, otherwise it will be confusing to have two sites for docs. Only the first one is suggested by google, for me at least. |
Done: root@tla:/etc/apache2/sites-enabled# tail -7 default-ssl.conf
Redirect 301 /tlaps https://proofs.tlapl.us/
</VirtualHost>
</IfModule> |
|
@lemmy, this works partially. Paths are different, redirects should consider this, IMO. For example Google suggests https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html Which is redirected to https://proofs.tlapl.us//content/Download/Binaries.html and gets 404. |
|
Do you know how to set this up in Apache 2? |
|
Maybe it is enough to replace with ? |
|
Please try again and let me know: root@tla:/etc/apache2/sites-enabled# tail -7 default-ssl.conf
Redirect 301 /tlaps https://proofs.tlapl.us/doc/web
</VirtualHost>
</IfModule> |
|
Looks good now. Thanks! |
doc/web/content/Download/Source.html
Outdated
| @@ -21,158 +21,33 @@ | |||
| <h2>Generic Instructions</h2> | |||
|
|
|||
| <p>These instructions apply to any UNIX-like system, including | |||
| GNU/Linux, most BSD variants, Solaris, Cygwin on Windows, | |||
| GNU/Linux, most BSD variants, Solaris, WSL and Cygwin on Windows, | |||
There was a problem hiding this comment.
Do we want to remove mention of Cygwin here and focus on WSL support?
There was a problem hiding this comment.
Thanks, I removed the mention of Cygwin.
| @@ -21,25 +21,25 @@ <h2><img class="blogo" src="images/logo_linux35.png" | |||
| alt="[Tux]"/>Linux</h2> | |||
| <p class="first"> The package: | |||
| <code><a type="application/x-executable" | |||
| href="https://github.com/tlaplus/tlapm/releases/latest/download/tlaps-1.4.5-x86_64-linux-gnu-inst.bin">tlaps-1.4.5-x86_64-linux-gnu-inst.bin</a></code> | |||
| href="https://github.com/tlaplus/tlapm/releases/download/202210041448/tlaps-1.5.0-x86_64-linux-gnu-inst.bin">tlaps-1.5.0-x86_64-linux-gnu-inst.bin</a></code> | |||
There was a problem hiding this comment.
In the (near) future when we switch to a rolling release model I suppose we will want to use the /latest/ tag along with a link to a binary that does not have the version in the name.
There was a problem hiding this comment.
I agree. This will have to be changed in the future.
For now, I just wanted to keep links valid after a new release is made.
Signed-off-by: Karolis Petrauskas <[email protected]>
|
@lemmy, @ahelwer, the MacOS version cannot be built anymore. The old Isabelle (2011) does not work with the ARM chips. The question:
|
|
Can we split the macOS build into intel and arm64? |
|
I think we will have to. Maybe for now, we can stick to |
|
Is there a way to do cross-compilation instead of having to run the build on an intel mac? |
|
I don't know; I never tried to do that. |
|
Are we forced to compile on |
Signed-off-by: Karolis Petrauskas <[email protected]>
|
It works with |
Fixes #123.