CI: skip source code build when only docs are modified

[yzhang-23]

I think we should skip the source code build step in CI in a docs update PR (only files under docs/ are modified), and vice versa, skip the docs build step if no files under docs/ are modified. This is easy to implement: just adding conditions (whether (only) the files under docs/ have been modified?) to trigger the corresponding CI actions (source build or docs build).
Obviously these issues are not critical. We can fix them later.