search

coq-community / sudoku

A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
https://coq-community.org/sudoku/
GNU Lesser General Public License v2.1
20 stars 3 forks source link

Generation of JavaScript and deployment #7

Closed palmskog closed 3 years ago

palmskog commented 3 years ago

When this repository is checked out, there is a dead symlink Html/Sudoku.js. The symlink points to a file that may be created by compilation using js_of_ocaml. This causes all kinds of havoc for opam packaging, and possibly for other packaging systems too.

The easiest solution is probably to just move all files tracked in the Html directory to the root directory. Then, a packaging or deployment process can just move the relevant files (SudokuBoard.js, Sudoku.css, Sudoku.html, Sudoku.js) to some other location after compilation.

To demonstrate what this project does, I suggest setting up a deployment process for every commit to master, so that the branch gh-pages holds the HTML/CSS/JS files above in the root. Then, we can activate GitHub pages and browse the Sudoku interface using the URL https://coq-community.org/sudoku/Sudoku.html

It is likely one can use a downscaled version of the hydra-battles deployment: https://github.com/coq-community/hydra-battles/blob/master/.github/workflows/build-documentation.yml

thery commented 3 years ago

@palmskog Thanks for taking some time to look into this. Feel free to change anything if it makes life easier

palmskog commented 3 years ago

@thery indeed I might take a look at addressing deployment automation soon (maybe next week), but in the meantime, I think #6 is ready to merge and will solve all your immediate problems with the project, such as checking with recent versions of Coq. So this issue is a more long term one.

thery commented 3 years ago

@palmskog would be nice too if the htnl would be generated somewhere in github.io

palmskog commented 3 years ago

@thery coq-community.github.io/project-name and coq-community.org/project-name are aliases, since we added the domain as an organization domain. So, for example, the hydra-battles generated pdf is deployed to the gh-pages branch of that repository, which makes it available using the following URLs:

thery commented 3 years ago

@palmskog Is this the doc?

palmskog commented 3 years ago

@thery that's one of the pieces of documentation, yes. It's a little different to set up an organization or personal website (my-name.github.io) and activate GitHub Pages for a particular project (usually shows up as my-name.github.io/repo-name). For example, when we set up the HTML deployment for this project to the gh-pages branch (just one out of many ways this can be done), GitHub Pages can be activated at: https://github.com/coq-community/sudoku/settings/pages

thery commented 3 years ago

it works :smile: sudoku now I have to understand how to make it automatically update like in hydra

thery commented 3 years ago

@palmskog not knowleadgeable enough with this tech, could not figure out where the pdf is automatically deployed in hydra. Try to grep gh-pages but there is nothing.

palmskog commented 3 years ago

@thery the push to the gh-pages branch is implicit. I will try to make a pull request with a configuration I think works during the afternoon. However, this configuration will erase any content that you manually put in the gh-pages branch. I assume that is OK?

thery commented 3 years ago

@palmskog Thanks. yes feel free to remove anything you want

palmskog commented 3 years ago

@thery looks like deployment works now:

I didn't make any symlink for index.html because I think there should be a dedicated index.html page (which links to Sudoku.html) for the project akin to this one: https://coq-community.org/reglang/

Once such a page has been put into the repo root, I can change the deployment configuration to include it.

palmskog commented 3 years ago

The workflow is now to always change the HTML/JS in the master branch. These changes are then pushed to gh-pages automatically, erasing all previous changes on that branch. Much more complex workflows are possible, but for a project of this size, I think it is the most reasonable one.

thery commented 3 years ago

too much technology for me. Thanks for fixing it!

palmskog commented 3 years ago

This repo should now be properly set up w.r.t. CI and deployment - hopefully with only minor changes required over the next few years in the course of regular maintenance. So I'm closing this issue, but feel free to reopen and ping me if something comes up.